---

Step * 1 1 2 of Lemma isect_prod_lemma


1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
5. x ∈ A × C
6. x ∈ A × B
⊢ <fst(x), snd(x)> ∈ A × B ⋂ C
BY
{ ((MemCD THEN Try (Complete (Auto))) THEN (Isect2CD THEN Try (Complete (Auto))) THEN Thin (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  x  :  A  \mtimes{}  B  \mcap{}  A  \mtimes{}  C
5.  x  \mmember{}  A  \mtimes{}  C
6.  x  \mmember{}  A  \mtimes{}  B
\mvdash{}  <fst(x),  snd(x)>  \mmember{}  A  \mtimes{}  B  \mcap{}  C


By

---

Latex:
((MemCD  THEN  Try  (Complete  (Auto)))
  THEN  (Isect2CD  THEN  Try  (Complete  (Auto)))
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index