---

Step * of Lemma isect2_decomp

∀[t1,t2:Type]. ∀[x:t1 ⋂ t2].  ((x ∈ t1) ∧ (x ∈ t2))
BY
{ Auto }

1
1. t1 : Type
2. t2 : Type
3. x : t1 ⋂ t2
⊢ x ∈ t1

2
1. t1 : Type
2. t2 : Type
3. x : t1 ⋂ t2
4. x ∈ t1
⊢ x ∈ t2

---

Latex:

---

Latex:
\mforall{}[t1,t2:Type].  \mforall{}[x:t1  \mcap{}  t2].    ((x  \mmember{}  t1)  \mwedge{}  (x  \mmember{}  t2))


By

---

Latex:
Auto

---

Home Index