---

Step * 1 1 1 of Lemma pgeo-psep-sym


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
11. s1 : r ≠ q
12. s4 : l ≠ p ∨ q
13. s3 : q ≠ r
14. p ≠ r
15. l ∧ p ∨ q ≠ q ∨ r
⊢ q ≠ p
BY
{ (((InstLemma `pgeo-meet-implies-plsep` [⌜g⌝;⌜l⌝;⌜p ∨ q⌝;⌜q ∨ r⌝;⌜s4⌝]⋅ THENA Auto)
    THEN (InstHyp [⌜p⌝] (-1)⋅ THENA Auto)
    )
   THEN InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜p⌝;⌜q⌝;⌜q ∨ r⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  p  :  Point
3.  q  :  Point
4.  s  :  p  \mneq{}  q
5.  l  :  Line
6.  p  I  l
7.  q  \mneq{}  l
8.  r  :  Point
9.  r  I  l
10.  r  \mneq{}  p  \mvee{}  q
11.  s1  :  r  \mneq{}  q
12.  s4  :  l  \mneq{}  p  \mvee{}  q
13.  s3  :  q  \mneq{}  r
14.  p  \mneq{}  r
15.  l  \mwedge{}  p  \mvee{}  q  \mneq{}  q  \mvee{}  r
\mvdash{}  q  \mneq{}  p


By

---

Latex:
(((InstLemma  `pgeo-meet-implies-plsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p  \mvee{}  q\mkleeneclose{};\mkleeneopen{}q  \mvee{}  r\mkleeneclose{};\mkleeneopen{}s4\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
    )
  THEN  InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}q  \mvee{}  r\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index