---

Step * 4 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,b,c:EType].  (e-isect(a;e-isect(b;c)) = e-isect(e-isect(a;b);c) ∈ EType)
4. a : Base
5. a1 : Base
6. a = a1 ∈ (A,B:Type//A ≡ B)
7. a ∈ Type
8. a1 ∈ Type
9. a ⊆r a1
10. a1 ⊆r a
11. b : Base
12. b1 : Base
13. b = b1 ∈ (A,B:Type//A ≡ B)
14. b ∈ Type
15. b1 ∈ Type
16. b ⊆r b1
17. b1 ⊆r b
18. c : Base
19. c1 : Base
20. c = c1 ∈ (A,B:Type//A ≡ B)
21. c ∈ Type
22. c1 ∈ Type
23. c ⊆r c1
24. c1 ⊆r c
25. a3 : a
⊢ a3 ∈ a1 ⋃ b1 ⋃ c1
BY
{ ((BUnionLeft THEN Try (BUnionLeft)) 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.  \mforall{}[a,b,c:EType].    (e-isect(a;e-isect(b;c))  =  e-isect(e-isect(a;b);c))
4.  a  :  Base
5.  a1  :  Base
6.  a  =  a1
7.  a  \mmember{}  Type
8.  a1  \mmember{}  Type
9.  a  \msubseteq{}r  a1
10.  a1  \msubseteq{}r  a
11.  b  :  Base
12.  b1  :  Base
13.  b  =  b1
14.  b  \mmember{}  Type
15.  b1  \mmember{}  Type
16.  b  \msubseteq{}r  b1
17.  b1  \msubseteq{}r  b
18.  c  :  Base
19.  c1  :  Base
20.  c  =  c1
21.  c  \mmember{}  Type
22.  c1  \mmember{}  Type
23.  c  \msubseteq{}r  c1
24.  c1  \msubseteq{}r  c
25.  a3  :  a
\mvdash{}  a3  \mmember{}  a1  \mcup{}  b1  \mcup{}  c1


By

---

Latex:
((BUnionLeft  THEN  Try  (BUnionLeft))  THEN  Auto)

---

Home Index