Metamath Proof Explorer

Theorem 5oai

Description: Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). (Contributed by NM, 5-May-2000) (New usage is discouraged.)

Ref Expression
Hypotheses 5oa.1 ⊢ 𝐴 ∈ Cℋ
5oa.2 ⊢ 𝐵 ∈ Cℋ
5oa.3 ⊢ 𝐶 ∈ Cℋ
5oa.4 ⊢ 𝐷 ∈ Cℋ
5oa.5 ⊢ 𝐹 ∈ Cℋ
5oa.6 ⊢ 𝐺 ∈ Cℋ
5oa.7 ⊢ 𝑅 ∈ Cℋ
5oa.8 ⊢ 𝑆 ∈ Cℋ
5oa.9 ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐵 )
5oa.10 ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐷 )
5oa.11 ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝐺 )
5oa.12 ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝑆 )
Assertion 5oai ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( ( 𝐹 ∨ℋ 𝐺 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 5oa.1 ⊢ 𝐴 ∈ Cℋ
2 5oa.2 ⊢ 𝐵 ∈ Cℋ
3 5oa.3 ⊢ 𝐶 ∈ Cℋ
4 5oa.4 ⊢ 𝐷 ∈ Cℋ
5 5oa.5 ⊢ 𝐹 ∈ Cℋ
6 5oa.6 ⊢ 𝐺 ∈ Cℋ
7 5oa.7 ⊢ 𝑅 ∈ Cℋ
8 5oa.8 ⊢ 𝑆 ∈ Cℋ
9 5oa.9 ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐵 )
10 5oa.10 ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐷 )
11 5oa.11 ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝐺 )
12 5oa.12 ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝑆 )
13 1 2 osumi ⊢ ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
14 9 13 ax-mp ⊢ ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 )
15 3 4 osumi ⊢ ( 𝐶 ⊆ ( ⊥ ‘ 𝐷 ) → ( 𝐶 +ℋ 𝐷 ) = ( 𝐶 ∨ℋ 𝐷 ) )
16 10 15 ax-mp ⊢ ( 𝐶 +ℋ 𝐷 ) = ( 𝐶 ∨ℋ 𝐷 )
17 14 16 ineq12i ⊢ ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) )
18 5 6 osumi ⊢ ( 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) → ( 𝐹 +ℋ 𝐺 ) = ( 𝐹 ∨ℋ 𝐺 ) )
19 11 18 ax-mp ⊢ ( 𝐹 +ℋ 𝐺 ) = ( 𝐹 ∨ℋ 𝐺 )
20 7 8 osumi ⊢ ( 𝑅 ⊆ ( ⊥ ‘ 𝑆 ) → ( 𝑅 +ℋ 𝑆 ) = ( 𝑅 ∨ℋ 𝑆 ) )
21 12 20 ax-mp ⊢ ( 𝑅 +ℋ 𝑆 ) = ( 𝑅 ∨ℋ 𝑆 )
22 19 21 ineq12i ⊢ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) = ( ( 𝐹 ∨ℋ 𝐺 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) )
23 17 22 ineq12i ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( ( 𝐹 ∨ℋ 𝐺 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) )
24 1 chshii ⊢ 𝐴 ∈ Sℋ
25 2 chshii ⊢ 𝐵 ∈ Sℋ
26 3 chshii ⊢ 𝐶 ∈ Sℋ
27 4 chshii ⊢ 𝐷 ∈ Sℋ
28 5 chshii ⊢ 𝐹 ∈ Sℋ
29 6 chshii ⊢ 𝐺 ∈ Sℋ
30 7 chshii ⊢ 𝑅 ∈ Sℋ
31 8 chshii ⊢ 𝑆 ∈ Sℋ
32 24 25 26 27 28 29 30 31 5oalem7 ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) )
33 23 32 eqsstrri ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( ( 𝐹 ∨ℋ 𝐺 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ⊆ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) )
34 24 26 shscli ⊢ ( 𝐴 +ℋ 𝐶 ) ∈ Sℋ
35 25 27 shscli ⊢ ( 𝐵 +ℋ 𝐷 ) ∈ Sℋ
36 34 35 shincli ⊢ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∈ Sℋ
37 24 30 shscli ⊢ ( 𝐴 +ℋ 𝑅 ) ∈ Sℋ
38 25 31 shscli ⊢ ( 𝐵 +ℋ 𝑆 ) ∈ Sℋ
39 37 38 shincli ⊢ ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∈ Sℋ
40 26 30 shscli ⊢ ( 𝐶 +ℋ 𝑅 ) ∈ Sℋ
41 27 31 shscli ⊢ ( 𝐷 +ℋ 𝑆 ) ∈ Sℋ
42 40 41 shincli ⊢ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∈ Sℋ
43 39 42 shscli ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ∈ Sℋ
44 36 43 shincli ⊢ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
45 24 28 shscli ⊢ ( 𝐴 +ℋ 𝐹 ) ∈ Sℋ
46 25 29 shscli ⊢ ( 𝐵 +ℋ 𝐺 ) ∈ Sℋ
47 45 46 shincli ⊢ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∈ Sℋ
48 28 30 shscli ⊢ ( 𝐹 +ℋ 𝑅 ) ∈ Sℋ
49 29 31 shscli ⊢ ( 𝐺 +ℋ 𝑆 ) ∈ Sℋ
50 48 49 shincli ⊢ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ∈ Sℋ
51 39 50 shscli ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ∈ Sℋ
52 47 51 shincli ⊢ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
53 26 28 shscli ⊢ ( 𝐶 +ℋ 𝐹 ) ∈ Sℋ
54 27 29 shscli ⊢ ( 𝐷 +ℋ 𝐺 ) ∈ Sℋ
55 53 54 shincli ⊢ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∈ Sℋ
56 42 50 shscli ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ∈ Sℋ
57 55 56 shincli ⊢ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
58 52 57 shscli ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ∈ Sℋ
59 44 58 shincli ⊢ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ∈ Sℋ
60 26 59 shscli ⊢ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ∈ Sℋ
61 24 60 shincli ⊢ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ∈ Sℋ
62 25 61 shsleji ⊢ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) )
63 26 59 shsleji ⊢ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ⊆ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) )
64 1 3 chsleji ⊢ ( 𝐴 +ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐶 )
65 2 4 chsleji ⊢ ( 𝐵 +ℋ 𝐷 ) ⊆ ( 𝐵 ∨ℋ 𝐷 )
66 ss2in ⊢ ( ( ( 𝐴 +ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐵 +ℋ 𝐷 ) ⊆ ( 𝐵 ∨ℋ 𝐷 ) ) → ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) )
67 64 65 66 mp2an ⊢ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) )
68 39 42 shsleji ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) )
69 3 7 chsleji ⊢ ( 𝐶 +ℋ 𝑅 ) ⊆ ( 𝐶 ∨ℋ 𝑅 )
70 4 8 chsleji ⊢ ( 𝐷 +ℋ 𝑆 ) ⊆ ( 𝐷 ∨ℋ 𝑆 )
71 ss2in ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ⊆ ( 𝐶 ∨ℋ 𝑅 ) ∧ ( 𝐷 +ℋ 𝑆 ) ⊆ ( 𝐷 ∨ℋ 𝑆 ) ) → ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) )
72 69 70 71 mp2an ⊢ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) )
73 26 30 shjshcli ⊢ ( 𝐶 ∨ℋ 𝑅 ) ∈ Sℋ
74 27 31 shjshcli ⊢ ( 𝐷 ∨ℋ 𝑆 ) ∈ Sℋ
75 73 74 shincli ⊢ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∈ Sℋ
76 42 75 39 shlej2i ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) → ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) )
77 72 76 ax-mp ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) )
78 1 7 chsleji ⊢ ( 𝐴 +ℋ 𝑅 ) ⊆ ( 𝐴 ∨ℋ 𝑅 )
79 2 8 chsleji ⊢ ( 𝐵 +ℋ 𝑆 ) ⊆ ( 𝐵 ∨ℋ 𝑆 )
80 ss2in ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ⊆ ( 𝐴 ∨ℋ 𝑅 ) ∧ ( 𝐵 +ℋ 𝑆 ) ⊆ ( 𝐵 ∨ℋ 𝑆 ) ) → ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) )
81 78 79 80 mp2an ⊢ ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) )
82 24 30 shjshcli ⊢ ( 𝐴 ∨ℋ 𝑅 ) ∈ Sℋ
83 25 31 shjshcli ⊢ ( 𝐵 ∨ℋ 𝑆 ) ∈ Sℋ
84 82 83 shincli ⊢ ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∈ Sℋ
85 39 84 75 shlej1i ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) → ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) )
86 81 85 ax-mp ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) )
87 77 86 sstri ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) )
88 68 87 sstri ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) )
89 ss2in ⊢ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∧ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) → ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) )
90 67 88 89 mp2an ⊢ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) )
91 52 57 shsleji ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) )
92 3 5 chsleji ⊢ ( 𝐶 +ℋ 𝐹 ) ⊆ ( 𝐶 ∨ℋ 𝐹 )
93 4 6 chsleji ⊢ ( 𝐷 +ℋ 𝐺 ) ⊆ ( 𝐷 ∨ℋ 𝐺 )
94 ss2in ⊢ ( ( ( 𝐶 +ℋ 𝐹 ) ⊆ ( 𝐶 ∨ℋ 𝐹 ) ∧ ( 𝐷 +ℋ 𝐺 ) ⊆ ( 𝐷 ∨ℋ 𝐺 ) ) → ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) )
95 92 93 94 mp2an ⊢ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) )
96 42 50 shsleji ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) )
97 5 7 chsleji ⊢ ( 𝐹 +ℋ 𝑅 ) ⊆ ( 𝐹 ∨ℋ 𝑅 )
98 6 8 chsleji ⊢ ( 𝐺 +ℋ 𝑆 ) ⊆ ( 𝐺 ∨ℋ 𝑆 )
99 ss2in ⊢ ( ( ( 𝐹 +ℋ 𝑅 ) ⊆ ( 𝐹 ∨ℋ 𝑅 ) ∧ ( 𝐺 +ℋ 𝑆 ) ⊆ ( 𝐺 ∨ℋ 𝑆 ) ) → ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ⊆ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
100 97 98 99 mp2an ⊢ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ⊆ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) )
101 28 30 shjshcli ⊢ ( 𝐹 ∨ℋ 𝑅 ) ∈ Sℋ
102 29 31 shjshcli ⊢ ( 𝐺 ∨ℋ 𝑆 ) ∈ Sℋ
103 101 102 shincli ⊢ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ∈ Sℋ
104 50 103 42 shlej2i ⊢ ( ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ⊆ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) → ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) )
105 100 104 ax-mp ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
106 42 75 103 shlej1i ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) → ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) )
107 72 106 ax-mp ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
108 105 107 sstri ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
109 96 108 sstri ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
110 ss2in ⊢ ( ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∧ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) → ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) )
111 95 109 110 mp2an ⊢ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) )
112 3 5 chjcli ⊢ ( 𝐶 ∨ℋ 𝐹 ) ∈ Cℋ
113 4 6 chjcli ⊢ ( 𝐷 ∨ℋ 𝐺 ) ∈ Cℋ
114 112 113 chincli ⊢ ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∈ Cℋ
115 114 chshii ⊢ ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∈ Sℋ
116 75 103 shjshcli ⊢ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ∈ Sℋ
117 115 116 shincli ⊢ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∈ Sℋ
118 57 117 52 shlej2i ⊢ ( ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) → ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) )
119 111 118 ax-mp ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) )
120 1 5 chsleji ⊢ ( 𝐴 +ℋ 𝐹 ) ⊆ ( 𝐴 ∨ℋ 𝐹 )
121 2 6 chsleji ⊢ ( 𝐵 +ℋ 𝐺 ) ⊆ ( 𝐵 ∨ℋ 𝐺 )
122 ss2in ⊢ ( ( ( 𝐴 +ℋ 𝐹 ) ⊆ ( 𝐴 ∨ℋ 𝐹 ) ∧ ( 𝐵 +ℋ 𝐺 ) ⊆ ( 𝐵 ∨ℋ 𝐺 ) ) → ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) )
123 120 121 122 mp2an ⊢ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) )
124 39 50 shsleji ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) )
125 50 103 39 shlej2i ⊢ ( ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ⊆ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) → ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) )
126 100 125 ax-mp ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
127 39 84 103 shlej1i ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) → ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) )
128 81 127 ax-mp ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
129 126 128 sstri ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
130 124 129 sstri ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) )
131 ss2in ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∧ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) → ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) )
132 123 130 131 mp2an ⊢ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) )
133 1 5 chjcli ⊢ ( 𝐴 ∨ℋ 𝐹 ) ∈ Cℋ
134 2 6 chjcli ⊢ ( 𝐵 ∨ℋ 𝐺 ) ∈ Cℋ
135 133 134 chincli ⊢ ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∈ Cℋ
136 135 chshii ⊢ ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∈ Sℋ
137 84 103 shjshcli ⊢ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ∈ Sℋ
138 136 137 shincli ⊢ ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∈ Sℋ
139 52 138 117 shlej1i ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) → ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) )
140 132 139 ax-mp ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) )
141 119 140 sstri ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) )
142 91 141 sstri ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) )
143 ss2in ⊢ ( ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ⊆ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∧ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) → ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) )
144 90 142 143 mp2an ⊢ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) )
145 1 3 chjcli ⊢ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ
146 2 4 chjcli ⊢ ( 𝐵 ∨ℋ 𝐷 ) ∈ Cℋ
147 145 146 chincli ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∈ Cℋ
148 84 75 shjcli ⊢ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ∈ Cℋ
149 147 148 chincli ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∈ Cℋ
150 149 chshii ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∈ Sℋ
151 138 117 shjshcli ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ∈ Sℋ
152 150 151 shincli ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ∈ Sℋ
153 59 152 26 shlej2i ⊢ ( ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ⊆ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) → ( 𝐶 ∨ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ⊆ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) )
154 144 153 ax-mp ⊢ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ⊆ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) )
155 63 154 sstri ⊢ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ⊆ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) )
156 sslin ⊢ ( ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ⊆ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) → ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ⊆ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) )
157 155 156 ax-mp ⊢ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ⊆ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) )
158 26 152 shjshcli ⊢ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ∈ Sℋ
159 24 158 shincli ⊢ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) ∈ Sℋ
160 61 159 25 shlej2i ⊢ ( ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ⊆ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) → ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
161 157 160 ax-mp ⊢ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) )
162 62 161 sstri ⊢ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) )
163 33 162 sstri ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( ( 𝐹 ∨ℋ 𝐺 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( 𝐶 ∨ℋ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 ∨ℋ 𝐹 ) ∩ ( 𝐵 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 ∨ℋ 𝑅 ) ∩ ( 𝐵 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ∨ℋ ( ( ( 𝐶 ∨ℋ 𝐹 ) ∩ ( 𝐷 ∨ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 ∨ℋ 𝑅 ) ∩ ( 𝐷 ∨ℋ 𝑆 ) ) ∨ℋ ( ( 𝐹 ∨ℋ 𝑅 ) ∩ ( 𝐺 ∨ℋ 𝑆 ) ) ) ) ) ) ) ) )