---

Step * of Lemma Unique

∀g:BasicProjectivePlane. ∀[l,m:Line]. ∀[p,q:Point].  ¬((¬p ≡ q) ∧ (¬l ≡ m)) supposing p I l ∧ q I l ∧ p I m ∧ q I m
BY
{ ((((Auto THEN Unhide) THENA Auto) THEN UseProjAxioms) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:BasicProjectivePlane
    \mforall{}[l,m:Line].  \mforall{}[p,q:Point].    \mneg{}((\mneg{}p  \mequiv{}  q)  \mwedge{}  (\mneg{}l  \mequiv{}  m))  supposing  p  I  l  \mwedge{}  q  I  l  \mwedge{}  p  I  m  \mwedge{}  q  I  m


By

---

Latex:
((((Auto  THEN  Unhide)  THENA  Auto)  THEN  UseProjAxioms)  THEN  Auto)

---

Home Index