---

Step * 1 1 of Lemma Join


1. g : ProjectivePlaneStructure
2. p : Point
3. q : Point
4. s : p ≠ q
⊢ ∃l:Line. (p I l ∧ q I l)
BY
{ (GenConclTerm ⌜p ∨ q⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(GenConclTerm  \mkleeneopen{}p  \mvee{}  q\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index