Theorem mdslmd1lem1

Description: Lemma for mdslmd1i . (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslmd.1	⊢ 𝐴 ∈ Cℋ
	mdslmd.2	⊢ 𝐵 ∈ Cℋ
	mdslmd.3	⊢ 𝐶 ∈ Cℋ
	mdslmd.4	⊢ 𝐷 ∈ Cℋ
	mdslmd1lem.5	⊢ 𝑅 ∈ Cℋ
Assertion	mdslmd1lem1	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	⊢ 𝐴 ∈ Cℋ
2		mdslmd.2	⊢ 𝐵 ∈ Cℋ
3		mdslmd.3	⊢ 𝐶 ∈ Cℋ
4		mdslmd.4	⊢ 𝐷 ∈ Cℋ
5		mdslmd1lem.5	⊢ 𝑅 ∈ Cℋ
6	4 2	chincli	⊢ ( 𝐷 ∩ 𝐵 ) ∈ Cℋ
7	5 6 1	chlej1i	⊢ ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) → ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) )
8		simpr	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐵 𝑀ℋ* 𝐴 )
9		simpr	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ 𝐷 )
10		simpr	⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
11	1 2 4	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
12		dmdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
13	11 12	mpan	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
14	8 9 10 13	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
15	14	3expb	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
16	15	sseq2d	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) ↔ ( 𝑅 ∨ℋ 𝐴 ) ⊆ 𝐷 ) )
17	7 16	imbitrid	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) → ( 𝑅 ∨ℋ 𝐴 ) ⊆ 𝐷 ) )
18	17	adantld	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( 𝑅 ∨ℋ 𝐴 ) ⊆ 𝐷 ) )
19	18	imim1d	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
20		simpll	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) )
21		simpll	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ 𝐶 )
22	21	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ 𝐶 )
23	1 5	chub2i	⊢ 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐴 )
24	22 23	jctil	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐴 ) ∧ 𝐴 ⊆ 𝐶 ) )
25		ssin	⊢ ( ( 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐴 ) ∧ 𝐴 ⊆ 𝐶 ) ↔ 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐶 ) )
26	24 25	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐶 ) )
27		inss1	⊢ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐷
28		sstr	⊢ ( ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ∧ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐷 ) → 𝑅 ⊆ 𝐷 )
29	27 28	mpan2	⊢ ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) → 𝑅 ⊆ 𝐷 )
30		sstr	⊢ ( ( 𝑅 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
31	29 30	sylan	⊢ ( ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
32	31	ancoms	⊢ ( ( 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
33	32	adantll	⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
34	33	adantll	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
35	34	ad2ant2l	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
36	1 2	chub1i	⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
37	35 36	jctir	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
38	1 2	chjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
39	5 1 38	chlubi	⊢ ( ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
40	37 39	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
41		simprrl	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
42	41	adantr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
43	40 42	jca	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
44	5 1	chjcli	⊢ ( 𝑅 ∨ℋ 𝐴 ) ∈ Cℋ
45	44 3 38	chlubi	⊢ ( ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
46	43 45	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
47	1 2 44 3	mdslj1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐶 ) ∧ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
48	20 26 46 47	syl12anc	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
49		simplll	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 𝑀ℋ 𝐵 )
50		simplrl	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) )
51		ssin	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
52	50 51	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
53	52	ssrind	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) )
54		inindir	⊢ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) )
55	53 54	sseqtrdi	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
56		simprl	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 )
57	55 56	sstrd	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑅 )
58		inss2	⊢ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵
59		sstr	⊢ ( ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ∧ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵 ) → 𝑅 ⊆ 𝐵 )
60	58 59	mpan2	⊢ ( 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) → 𝑅 ⊆ 𝐵 )
61	60	ad2antll	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝑅 ⊆ 𝐵 )
62	1 2 5	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑅 ∈ Cℋ )
63		mdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑅 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐵 ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝑅 )
64	62 63	mpan	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐵 ) → ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝑅 )
65	49 57 61 64	syl3anc	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝑅 )
66	65	oveq1d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) = ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
67	48 66	eqtr2d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) = ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐵 ) )
68	67	ineq1d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
69		inindir	⊢ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) = ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) )
70	68 69	eqtr4di	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) )
71	52 23	jctil	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐴 ) ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ) )
72		ssin	⊢ ( ( 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐴 ) ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ) ↔ 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∩ ( 𝐶 ∩ 𝐷 ) ) )
73	71 72	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∩ ( 𝐶 ∩ 𝐷 ) ) )
74		ssinss1	⊢ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
75	74	ad2antrl	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
76	75	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
77	40 76	jca	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
78	3 4	chincli	⊢ ( 𝐶 ∩ 𝐷 ) ∈ Cℋ
79	44 78 38	chlubi	⊢ ( ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
80	77 79	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
81	1 2 44 78	mdslj1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
82	20 73 80 81	syl12anc	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
83	54	a1i	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
84	65 83	oveq12d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) = ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) )
85	82 84	eqtr2d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) = ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) )
86	70 85	sseq12d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ↔ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
87		simpllr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐵 𝑀ℋ* 𝐴 )
88		simplr	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ 𝐷 )
89	88	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ 𝐷 )
90	44 3	chub1i	⊢ ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 )
91	23 90	sstri	⊢ 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 )
92	89 91	jctil	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∧ 𝐴 ⊆ 𝐷 ) )
93		ssin	⊢ ( ( 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) )
94	92 93	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) )
95	44 78	chub1i	⊢ ( 𝑅 ∨ℋ 𝐴 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) )
96	23 95	sstri	⊢ 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) )
97	94 96	jctir	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∧ 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
98		ssin	⊢ ( ( 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∧ 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ↔ 𝐴 ⊆ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
99	97 98	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → 𝐴 ⊆ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
100		inss2	⊢ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ 𝐷
101		sstr	⊢ ( ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
102	100 101	mpan	⊢ ( 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
103	102	ad2antll	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
104	103	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
105	104 80	jca	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
106	44 3	chjcli	⊢ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∈ Cℋ
107	106 4	chincli	⊢ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∈ Cℋ
108	44 78	chjcli	⊢ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∈ Cℋ
109	107 108 38	chlubi	⊢ ( ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
110	105 109	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
111	1 2 107 108	mdslle1i	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ∧ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
112	87 99 110 111	syl3anc	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
113	86 112	bitr4d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
114	113	exbiri	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
115	114	a2d	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
116	19 115	syld	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑅 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑅 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑅 ∧ 𝑅 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )