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}}_{\mathscr{H}}$$
	5oa.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	5oa.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	5oa.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
	5oa.5	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
	5oa.6	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	5oa.7	$$⊢R\in {\mathbf{C}}_{\mathscr{H}}$$
	5oa.8	$$⊢S\in {\mathbf{C}}_{\mathscr{H}}$$
	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 }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\cap \left(\left(F{\vee }_{\mathscr{H}}G\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\subseteq B{\vee }_{\mathscr{H}}\left(A\cap \left(C{\vee }_{\mathscr{H}}\left(\left(\left(\left(A{\vee }_{\mathscr{H}}C\right)\cap \left(B{\vee }_{\mathscr{H}}D\right)\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}R\right)\cap \left(B{\vee }_{\mathscr{H}}S\right)\right){\vee }_{\mathscr{H}}\left(\left(C{\vee }_{\mathscr{H}}R\right)\cap \left(D{\vee }_{\mathscr{H}}S\right)\right)\right)\right)\cap \left(\left(\left(\left(A{\vee }_{\mathscr{H}}F\right)\cap \left(B{\vee }_{\mathscr{H}}G\right)\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}R\right)\cap \left(B{\vee }_{\mathscr{H}}S\right)\right){\vee }_{\mathscr{H}}\left(\left(F{\vee }_{\mathscr{H}}R\right)\cap \left(G{\vee }_{\mathscr{H}}S\right)\right)\right)\right){\vee }_{\mathscr{H}}\left(\left(\left(C{\vee }_{\mathscr{H}}F\right)\cap \left(D{\vee }_{\mathscr{H}}G\right)\right)\cap \left(\left(\left(C{\vee }_{\mathscr{H}}R\right)\cap \left(D{\vee }_{\mathscr{H}}S\right)\right){\vee }_{\mathscr{H}}\left(\left(F{\vee }_{\mathscr{H}}R\right)\cap \left(G{\vee }_{\mathscr{H}}S\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof

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