---

Step * 1 of Lemma Join


1. g : ProjectivePlaneStructure
2. p : Point
3. q : Point
4. p ≠ q
⊢ ∃l:Line. (p I l ∧ q I l)
BY
{ RenameVar `s' (-1) }

1
1. g : ProjectivePlaneStructure
2. p : Point
3. q : Point
4. s : p ≠ q
⊢ ∃l:Line. (p I l ∧ q I l)

---

Latex:

---

Latex:

1.  g  :  ProjectivePlaneStructure
2.  p  :  Point
3.  q  :  Point
4.  p  \mneq{}  q
\mvdash{}  \mexists{}l:Line.  (p  I  l  \mwedge{}  q  I  l)


By

---

Latex:
RenameVar  `s'  (-1)

---

Home Index