Theorem mdslmd1lem2

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	mdslmd1lem2	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )

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		ssrin	⊢ ( 𝑅 ⊆ 𝐷 → ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) )
7	6	adantl	⊢ ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) )
8	7	imim1i	⊢ ( ( ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
9		simpllr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐵 𝑀ℋ* 𝐴 )
10	3 5	chub2i	⊢ 𝐶 ⊆ ( 𝑅 ∨ℋ 𝐶 )
11		sstr	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝑅 ∨ℋ 𝐶 ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
12	10 11	mpan2	⊢ ( 𝐴 ⊆ 𝐶 → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
13	12	ad2antrr	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
14	13	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
15		simplr	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ 𝐷 )
16	15	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ 𝐷 )
17	14 16	ssind	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) )
18		ssin	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
19	3 4	chincli	⊢ ( 𝐶 ∩ 𝐷 ) ∈ Cℋ
20	19 5	chub2i	⊢ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) )
21		sstr	⊢ ( ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
22	20 21	mpan2	⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
23	18 22	sylbi	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
24	23	adantr	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
25	24	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
26	17 25	ssind	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
27		inss2	⊢ ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ 𝐷
28		sstr	⊢ ( ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
29	27 28	mpan	⊢ ( 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
30	29	ad2antll	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
31	30	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
32		sstr	⊢ ( ( 𝑅 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
33	32	ancoms	⊢ ( ( 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑅 ⊆ 𝐷 ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
34	33	ad2ant2l	⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
35	34	adantll	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
36	35	adantll	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
37		ssinss1	⊢ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
38	37	ad2antrl	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
39	38	ad2antlr	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
40	36 39	jca	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
41	1 2	chjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
42	5 19 41	chlubi	⊢ ( ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
43	40 42	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
44	31 43	jca	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
45	5 3	chjcli	⊢ ( 𝑅 ∨ℋ 𝐶 ) ∈ Cℋ
46	45 4	chincli	⊢ ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∈ Cℋ
47	5 19	chjcli	⊢ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∈ Cℋ
48	46 47 41	chlubi	⊢ ( ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
49	44 48	sylib	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
50	1 2 46 47	mdslle1i	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ∧ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
51	9 26 49 50	syl3anc	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
52		inindir	⊢ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) = ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) )
53		sstr	⊢ ( ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ 𝑅 )
54	18 53	sylanb	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ 𝑅 )
55	54	ad2ant2r	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ 𝑅 )
56		simplll	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ 𝐶 )
57	55 56	ssind	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( 𝑅 ∩ 𝐶 ) )
58		simplrl	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
59	35 58	jca	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
60	5 3 41	chlubi	⊢ ( ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
61	59 60	sylib	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
62	57 61	jca	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐴 ⊆ ( 𝑅 ∩ 𝐶 ) ∧ ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
63	1 2 5 3	mdslj1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝑅 ∩ 𝐶 ) ∧ ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
64	62 63	sylan2	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
65	64	anassrs	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
66	65	ineq1d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
67	52 66	syl5req	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) )
68	18	biimpi	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
69	68	adantr	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
70	54 69	ssind	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) )
71	33	adantll	⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
72	37	ad2antrr	⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
73	71 72	jca	⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
74	73 42	sylib	⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
75	70 74	anim12i	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) ∧ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
76	75	an4s	⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
77	1 2 5 19	mdslj1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
78	76 77	sylan2	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
79	78	anassrs	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
80		inindir	⊢ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) )
81	80	a1i	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
82	81	oveq2d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) )
83	79 82	eqtr2d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) = ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) )
84	67 83	sseq12d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
85	51 84	bitr4d	⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
86	85	exbiri	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
87	86	a2d	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
88	8 87	syl5	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )