---

Step * 1 of Lemma LP-sep-or2

.....assertion..... 
1. g : ProjectivePlaneStructure
2. l : Line
3. p : Point
4. q : Point
5. p ≠ l
⊢ l ≠ p
BY
{ (Unfold `pgeo-lpsep` 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  g  :  ProjectivePlaneStructure
2.  l  :  Line
3.  p  :  Point
4.  q  :  Point
5.  p  \mneq{}  l
\mvdash{}  l  \mneq{}  p


By

---

Latex:
(Unfold  `pgeo-lpsep`  0  THEN  Auto)

---

Home Index