---

Step * of Lemma plsep-join-implies

∀g:ProjectivePlane. ∀p,q,r:Point. ∀s:p ≠ q.  (r ≠ p ∨ q ⇒ {q ≠ r ∧ p ≠ r})
BY
{ (Auto
   THEN (InstLemma `Join` [⌜g⌝;⌜p⌝;⌜q⌝]⋅ THEN Auto)
   THEN D -1
   THEN InstLemma `pgeo-join-to-line-2` [⌜g⌝;⌜p⌝;⌜q⌝;⌜l⌝;⌜s⌝]⋅
   THEN Auto
   THEN D 0) }

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
⊢ q ≠ r

2
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

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p,q,r:Point.  \mforall{}s:p  \mneq{}  q.    (r  \mneq{}  p  \mvee{}  q  {}\mRightarrow{}  \{q  \mneq{}  r  \mwedge{}  p  \mneq{}  r\})


By

---

Latex:
(Auto
  THEN  (InstLemma  `Join`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -1
  THEN  InstLemma  `pgeo-join-to-line-2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0)

---

Home Index