---

Step * of Lemma pgeo-join-implies-plsep

∀g:BasicProjectivePlane. ∀a,b,c:Point. ∀s:a ≠ b.  (c ≠ a ∨ b ⇒ (∀l:Line. ((a I l ∧ b I l) ⇒ c ≠ l)))
BY
{ (Auto THEN ((InstLemma `PL-sep-or` [⌜g⌝;⌜c⌝;⌜a ∨ b⌝;⌜l⌝]⋅ THEN Auto) THEN D -1) THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  ((InstLemma  `PL-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a  \mvee{}  b\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1)  THEN  Auto)

---

Home Index