---

Step * of Lemma pgeo-plsep-implies-join

∀g:BasicProjectivePlane. ∀c:Point. ∀l:Line.  (c ≠ l ⇒ (∀a,b:Point. ∀s:a ≠ b.  ((a I l ∧ b I l) ⇒ c ≠ a ∨ b)))
BY
{ Auto }

1
1. g : BasicProjectivePlane
2. c : Point
3. l : Line
4. c ≠ l
5. a : Point
6. b : Point
7. s : a ≠ b
8. a I l
9. b I l
⊢ c ≠ a ∨ b

---

Latex:

---

Latex:
\mforall{}g:BasicProjectivePlane.  \mforall{}c:Point.  \mforall{}l:Line.
    (c  \mneq{}  l  {}\mRightarrow{}  (\mforall{}a,b:Point.  \mforall{}s:a  \mneq{}  b.    ((a  I  l  \mwedge{}  b  I  l)  {}\mRightarrow{}  c  \mneq{}  a  \mvee{}  b)))


By

---

Latex:
Auto

---

Home Index