---

Step * 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. l1 : Line
10. q ≠ l1
⊢ ∃r:Point. (r I l ∧ r ≠ q ∨ p)
BY
{ (((RenameVar`m' (9) THEN InstLemma `pgeo-plsep-to-lsep` [⌜g⌝;⌜m⌝;⌜l⌝;⌜q⌝]⋅ THEN Auto)
    THEN InstLemma `Meet` [⌜g⌝;⌜l⌝;⌜m⌝]⋅
    THEN Auto)
   THEN (ExRepD THEN RenameVar `r' (12))
   THEN InstConcl [⌜r⌝]⋅
   THEN Auto) }

1
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

---

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.  l1  :  Line
10.  q  \mneq{}  l1
\mvdash{}  \mexists{}r:Point.  (r  I  l  \mwedge{}  r  \mneq{}  q  \mvee{}  p)


By

---

Latex:
(((RenameVar`m'  (9)  THEN  InstLemma  `pgeo-plsep-to-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)
    THEN  InstLemma  `Meet`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  (ExRepD  THEN  RenameVar  `r'  (12))
  THEN  InstConcl  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index