---

Step * 2 of Lemma pgeo-plsep-iff-all-psep


1. g : ProjectivePlane
2. p : Point
3. l : Line
4. ∀q:Point. (q I l ⇒ p ≠ q)
⊢ p ≠ l
BY
{ ((InstLemma `pgeo-three-lines-axiom` [⌜g⌝;⌜p⌝]⋅ THENA Auto) THEN ExRepD) }

1
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. ∀q:Point. (q I l ⇒ p ≠ q)
5. l1 : Line
6. m : Line
7. n : Line
8. p I l1
9. p I m
10. p I n
11. l1 ≠ m
12. m ≠ n
13. n ≠ l1
⊢ p ≠ l

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  p  :  Point
3.  l  :  Line
4.  \mforall{}q:Point.  (q  I  l  {}\mRightarrow{}  p  \mneq{}  q)
\mvdash{}  p  \mneq{}  l


By

---

Latex:
((InstLemma  `pgeo-three-lines-axiom`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index