---

Step * of Lemma isect_prod_lemma

∀[A,B,C:Type].  (A × B ⋂ A × C ⊆r (A × B ⋂ C))
BY
{ (Intros THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
⊢ x ∈ A × B ⋂ C

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    (A  \mtimes{}  B  \mcap{}  A  \mtimes{}  C  \msubseteq{}r  (A  \mtimes{}  B  \mcap{}  C))


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto))

---

Home Index