# 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 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
5oa.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
5oa.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
5oa.4 ${⊢}{D}\in {\mathbf{C}}_{ℋ}$
5oa.5 ${⊢}{F}\in {\mathbf{C}}_{ℋ}$
5oa.6 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
5oa.7 ${⊢}{R}\in {\mathbf{C}}_{ℋ}$
5oa.8 ${⊢}{S}\in {\mathbf{C}}_{ℋ}$
5oa.9 ${⊢}{A}\subseteq \perp \left({B}\right)$
5oa.10 ${⊢}{C}\subseteq \perp \left({D}\right)$
5oa.11 ${⊢}{F}\subseteq \perp \left({G}\right)$
5oa.12 ${⊢}{R}\subseteq \perp \left({S}\right)$
Assertion 5oai ${⊢}\left(\left({A}{\vee }_{ℋ}{B}\right)\cap \left({C}{\vee }_{ℋ}{D}\right)\right)\cap \left(\left({F}{\vee }_{ℋ}{G}\right)\cap \left({R}{\vee }_{ℋ}{S}\right)\right)\subseteq {B}{\vee }_{ℋ}\left({A}\cap \left({C}{\vee }_{ℋ}\left(\left(\left(\left({A}{\vee }_{ℋ}{C}\right)\cap \left({B}{\vee }_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{\vee }_{ℋ}{R}\right)\cap \left({B}{\vee }_{ℋ}{S}\right)\right){\vee }_{ℋ}\left(\left({C}{\vee }_{ℋ}{R}\right)\cap \left({D}{\vee }_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{\vee }_{ℋ}{F}\right)\cap \left({B}{\vee }_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{\vee }_{ℋ}{R}\right)\cap \left({B}{\vee }_{ℋ}{S}\right)\right){\vee }_{ℋ}\left(\left({F}{\vee }_{ℋ}{R}\right)\cap \left({G}{\vee }_{ℋ}{S}\right)\right)\right)\right){\vee }_{ℋ}\left(\left(\left({C}{\vee }_{ℋ}{F}\right)\cap \left({D}{\vee }_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{\vee }_{ℋ}{R}\right)\cap \left({D}{\vee }_{ℋ}{S}\right)\right){\vee }_{ℋ}\left(\left({F}{\vee }_{ℋ}{R}\right)\cap \left({G}{\vee }_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)$

### Proof

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