This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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