---

Step * 2 1 2 of Lemma pgeo-plsep-iff-all-psep


1. g : ProjectivePlane
2. p : Point
3. l : Line
4. ∀q:Point. (q I l ⇒ p ≠ q)
5. l1 : Line
6. m : Line
7. n : Line
8. p I l1
9. p I m
10. p I n
11. l1 ≠ m
12. m ≠ n
13. n ≠ l1
14. l ≠ m
⊢ p ≠ l
BY
{ ((((InstLemma `Meet` [⌜g⌝;⌜m⌝;⌜l⌝]⋅ THENA EAuto 1) THEN ExRepD) THEN (InstHyp [⌜p1⌝] (4)⋅ THENA Auto))
   THEN ((Assert m ≠ l BY EAuto 1) THEN RenameVar `s' (-1)⋅)
   THEN InstLemma `pgeo-lsep-implies-plsep` [⌜g⌝;⌜p⌝;⌜m⌝;⌜l⌝;⌜s⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  p  :  Point
3.  l  :  Line
4.  \mforall{}q:Point.  (q  I  l  {}\mRightarrow{}  p  \mneq{}  q)
5.  l1  :  Line
6.  m  :  Line
7.  n  :  Line
8.  p  I  l1
9.  p  I  m
10.  p  I  n
11.  l1  \mneq{}  m
12.  m  \mneq{}  n
13.  n  \mneq{}  l1
14.  l  \mneq{}  m
\mvdash{}  p  \mneq{}  l


By

---

Latex:
((((InstLemma  `Meet`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)  THEN  ExRepD)
    THEN  (InstHyp  [\mkleeneopen{}p1\mkleeneclose{}]  (4)\mcdot{}  THENA  Auto)
    )
  THEN  ((Assert  m  \mneq{}  l  BY  EAuto  1)  THEN  RenameVar  `s'  (-1)\mcdot{})
  THEN  InstLemma  `pgeo-lsep-implies-plsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index