---

Step * of Lemma pgeo-psep-sym

∀g:ProjectivePlane. ∀p,q:Point.  (p ≠ q ⇒ q ≠ p)
BY
{ (((Auto THEN Duplicate 4 THEN D -1)
    THEN RenameVar `s' (4)
    THEN InstLemma `plsep-implies-ptriangle` [⌜g⌝;⌜q⌝;⌜l⌝;⌜p⌝;⌜s⌝]⋅
    THEN Auto)
   THEN ExRepD
   ) }

1
1. g : ProjectivePlane
2. p : Point
3. q : Point
4. s : p ≠ q
5. l : Line
6. p I l
7. q ≠ l
8. r : Point
9. r I l
10. r ≠ p ∨ q
⊢ q ≠ p

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p,q:Point.    (p  \mneq{}  q  {}\mRightarrow{}  q  \mneq{}  p)


By

---

Latex:
(((Auto  THEN  Duplicate  4  THEN  D  -1)
    THEN  RenameVar  `s'  (4)
    THEN  InstLemma  `plsep-implies-ptriangle`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  ExRepD
  )

---

Home Index