---

Step * 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. l ≠ p ∨ q
⊢ q ≠ p
BY
{ (((InstLemma `plsep-join-implies` [⌜g⌝;⌜p⌝;⌜q⌝;⌜r⌝;⌜s⌝]⋅ THENA Auto) THEN ExRepD)
   THEN (RenameVar `s3' (-2) THEN RenameVar `s4' (12))
   THEN (InstLemma `use-triangle-axiom2` [⌜g⌝;⌜q⌝;⌜r⌝;⌜l⌝;⌜p ∨ q⌝;⌜s3⌝;⌜s4⌝]⋅ THENA 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. s4 : l ≠ p ∨ q
13. s3 : q ≠ r
14. p ≠ r
15. l ∧ p ∨ q ≠ q ∨ r
⊢ 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
11.  s1  :  r  \mneq{}  q
12.  l  \mneq{}  p  \mvee{}  q
\mvdash{}  q  \mneq{}  p


By

---

Latex:
(((InstLemma  `plsep-join-implies`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (RenameVar  `s3'  (-2)  THEN  RenameVar  `s4'  (12))
  THEN  (InstLemma  `use-triangle-axiom2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p  \mvee{}  q\mkleeneclose{};\mkleeneopen{}s3\mkleeneclose{};\mkleeneopen{}s4\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index