---

Step * 2 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
⊢ p ≠ r
BY
{ (Unfold `pgeo-psep` 0 THEN InstConcl [⌜l⌝]⋅ THEN Auto) }

1
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

---

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
\mvdash{}  p  \mneq{}  r


By

---

Latex:
(Unfold  `pgeo-psep`  0  THEN  InstConcl  [\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index