---

Step * 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
⊢ q ≠ p
BY
{ (((Assert r ≠ q BY (InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜q⌝;⌜r⌝;⌜l⌝]⋅ THEN Auto)) THEN RenameVar `s1' (-1))
   THEN InstLemma `pgeo-plsep-to-lsep` [⌜g⌝;⌜p ∨ q⌝;⌜l⌝;⌜r⌝]⋅
   THEN Auto) }

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
11. s1 : r ≠ q
12. l ≠ p ∨ q
⊢ q ≠ p

---

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
\mvdash{}  q  \mneq{}  p


By

---

Latex:
(((Assert  r  \mneq{}  q  BY
                  (InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto))
    THEN  RenameVar  `s1'  (-1)
    )
  THEN  InstLemma  `pgeo-plsep-to-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p  \mvee{}  q\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index