---

Step * of Lemma pgeo-three-lines-axiom

∀g:ProjectivePlaneStructure. ∀p:Point.  ∃l,m,n:Line. (p I l ∧ p I m ∧ p I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)
BY
{ ((Auto THEN UseWitness ⌜pgeo-three-line-axiom(p)⌝⋅) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructure.  \mforall{}p:Point.    \mexists{}l,m,n:Line.  (p  I  l  \mwedge{}  p  I  m  \mwedge{}  p  I  n  \mwedge{}  l  \mneq{}  m  \mwedge{}  m  \mneq{}  n  \mwedge{}  n  \mneq{}  l)


By

---

Latex:
((Auto  THEN  UseWitness  \mkleeneopen{}pgeo-three-line-axiom(p)\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index