---

Step * 1 of Lemma pgeo-lsep-or


1. g : BasicProjectivePlane
2. l : Line
3. m : Line
4. n : Line
5. l ≠ m
6. a : Point
7. a I l
8. a ≠ m
9. a ≠ n
⊢ l ≠ n ∨ n ≠ m
BY
{ (InstLemma `pgeo-plsep-to-lsep` [⌜g⌝;⌜n⌝;⌜l⌝;⌜a⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  BasicProjectivePlane
2.  l  :  Line
3.  m  :  Line
4.  n  :  Line
5.  l  \mneq{}  m
6.  a  :  Point
7.  a  I  l
8.  a  \mneq{}  m
9.  a  \mneq{}  n
\mvdash{}  l  \mneq{}  n  \mvee{}  n  \mneq{}  m


By

---

Latex:
(InstLemma  `pgeo-plsep-to-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index