---

Step * of Lemma line-implies-plsep-exists

∀g:ProjectivePlane. ∀l:Line.  ∃p:Point. p ≠ l
BY
{ ((Auto THEN InstLemma `pgeo-three-points-axiom` [⌜g⌝;⌜l⌝]⋅ THEN Auto)
   THEN ExRepD
   THEN InstLemma `point-implies-plsep-exists` [⌜g⌝;⌜a⌝]⋅
   THEN Auto) }

1
1. g : ProjectivePlane
2. l : Line
3. a : Point
4. b : Point
5. c : Point
6. a I l
7. b I l
8. c I l
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. ∃l:Line. a ≠ l
⊢ ∃p:Point. p ≠ l

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}l:Line.    \mexists{}p:Point.  p  \mneq{}  l


By

---

Latex:
((Auto  THEN  InstLemma  `pgeo-three-points-axiom`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  InstLemma  `point-implies-plsep-exists`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index