---

Step * 3 of Lemma type-lattice_wf


1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. a : Base
4. a1 : Base
5. a = a1 ∈ (A,B:Type//A ≡ B)
6. a ∈ Type
7. a1 ∈ Type
8. a ⊆r a1
9. a1 ⊆r a
10. b : Base
11. b1 : Base
12. b = b1 ∈ (A,B:Type//A ≡ B)
13. b ∈ Type
14. b1 ∈ Type
15. b ⊆r b1
16. b1 ⊆r b
17. c : Base
18. c1 : Base
19. c = c1 ∈ (A,B:Type//A ≡ B)
20. c ∈ Type
21. c1 ∈ Type
22. c ⊆r c1
23. c1 ⊆r c
24. x : a1 ⋂ b1 ⋂ c1
25. x ∈ c1
26. x ∈ a1 ⋂ b1
27. x ∈ b1
28. x ∈ a1
⊢ x ∈ b ⋂ c
BY
{ (Isect2CD THENL [(SubsumeC ⌜b1⌝⋅ THEN Auto); (SubsumeC ⌜c1⌝⋅ THEN Auto)]) }

---

Latex:

---

Latex:

1.  \mforall{}[a,b:EType].    (e-isect(a;b)  =  e-isect(b;a))
2.  \mforall{}[a,b:EType].    (e-union(a;b)  =  e-union(b;a))
3.  a  :  Base
4.  a1  :  Base
5.  a  =  a1
6.  a  \mmember{}  Type
7.  a1  \mmember{}  Type
8.  a  \msubseteq{}r  a1
9.  a1  \msubseteq{}r  a
10.  b  :  Base
11.  b1  :  Base
12.  b  =  b1
13.  b  \mmember{}  Type
14.  b1  \mmember{}  Type
15.  b  \msubseteq{}r  b1
16.  b1  \msubseteq{}r  b
17.  c  :  Base
18.  c1  :  Base
19.  c  =  c1
20.  c  \mmember{}  Type
21.  c1  \mmember{}  Type
22.  c  \msubseteq{}r  c1
23.  c1  \msubseteq{}r  c
24.  x  :  a1  \mcap{}  b1  \mcap{}  c1
25.  x  \mmember{}  c1
26.  x  \mmember{}  a1  \mcap{}  b1
27.  x  \mmember{}  b1
28.  x  \mmember{}  a1
\mvdash{}  x  \mmember{}  b  \mcap{}  c


By

---

Latex:
(Isect2CD  THENL  [(SubsumeC  \mkleeneopen{}b1\mkleeneclose{}\mcdot{}  THEN  Auto);  (SubsumeC  \mkleeneopen{}c1\mkleeneclose{}\mcdot{}  THEN  Auto)])

---

Home Index