---

Step * 1 1 of Lemma plsep-implies-ptriangle


1. g : ProjectivePlane
2. p : Point
3. l : Line
4. q : Point
5. s : q ≠ p
6. p ≠ l
7. q I l
8. q ≠ p
9. m : Line
10. q ≠ m
11. l ≠ m
12. r : Point
13. r I l
14. r I m
15. r I l
⊢ r ≠ q ∨ p
BY
{ (((Assert r ≠ q BY (InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜q⌝;⌜r⌝;⌜m⌝]⋅ THEN Auto)) THEN RenameVar `t1' (16))
   THEN ((InstLemma `use-triangle-axiom1` [⌜g⌝;⌜r⌝;⌜q⌝;⌜p⌝;⌜t1⌝;⌜s⌝]⋅ THEN Auto)
         THENA (InstLemma `pgeo-plsep-implies-join` [⌜g⌝;⌜p⌝;⌜l⌝]⋅ THEN Auto)
         )
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(((Assert  r  \mneq{}  q  BY
                  (InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto))
    THEN  RenameVar  `t1'  (16)
    )
  THEN  ((InstLemma  `use-triangle-axiom1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}t1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THEN  Auto)
              THENA  (InstLemma  `pgeo-plsep-implies-join`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  Auto)

---

Home Index