---

Step * 2 of Lemma LP-sep-or2


1. g : ProjectivePlaneStructure
2. l : Line
3. p : Point
4. q : Point
5. p ≠ l
6. l ≠ p
⊢ q ≠ l ∨ q ≠ p
BY
{ (InstLemma `LP-sep-or` [⌜g⌝;⌜l⌝;⌜p⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlaneStructure
2.  l  :  Line
3.  p  :  Point
4.  q  :  Point
5.  p  \mneq{}  l
6.  l  \mneq{}  p
\mvdash{}  q  \mneq{}  l  \mvee{}  q  \mneq{}  p


By

---

Latex:
(InstLemma  `LP-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index