---

Step * 1 of Lemma free-from-atom-pair


1. a : Atom1
2. X : Type
3. Y : Type
4. x : X
5. y : Y
6. a#x:X
7. a#y:Y
8. a#y:Y ∈ ℙ
9. a#x:X ∈ ℙ
⊢ a#<x, y>:X × Y
BY
{ (FreeFromAtomApElim ⌜x⌝⋅ THEN FreeFromAtomApElim ⌜y⌝⋅ THEN FreeFromAtomTriviality THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  Atom1
2.  X  :  Type
3.  Y  :  Type
4.  x  :  X
5.  y  :  Y
6.  a\#x:X
7.  a\#y:Y
8.  a\#y:Y  \mmember{}  \mBbbP{}
9.  a\#x:X  \mmember{}  \mBbbP{}
\mvdash{}  a\#<x,  y>:X  \mtimes{}  Y


By

---

Latex:
(FreeFromAtomApElim  \mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  FreeFromAtomApElim  \mkleeneopen{}y\mkleeneclose{}\mcdot{}  THEN  FreeFromAtomTriviality  THEN  Auto)\mcdot{}

---

Home Index