---

Step * 2 1 of Lemma plsep-join-implies


1. g : ProjectivePlane
2. p : Point
3. q : Point
4. r : Point
5. s : p ≠ q
6. r ≠ p ∨ q
7. l : Line
8. p I l
9. q I l
10. l ≡ p ∨ q
11. p I l
⊢ r ≠ l
BY
{ (((InstLemma `PL-sep-or` [⌜g⌝;⌜r⌝;⌜p ∨ q⌝;⌜l⌝]⋅ THEN Auto) THEN D -1 THEN Auto)
   THEN (Assert False BY
               D 10)
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(((InstLemma  `PL-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}p  \mvee{}  q\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  Auto)
  THEN  (Assert  False  BY
                          D  10)
  THEN  Auto)

---

Home Index