---

Step * of Lemma use-triangle-axiom2

∀g:ProjectivePlane. ∀p,q:Point. ∀l,m:Line. ∀s:p ≠ q. ∀s1:l ≠ m.  (p ≠ l ⇒ q ≠ m ⇒ p I m ⇒ q I l ⇒ l ∧ m ≠ p ∨ q)
BY
{ ((Auto THEN InstLemma `projective-plane-axioms` [⌜g⌝]⋅) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p,q:Point.  \mforall{}l,m:Line.  \mforall{}s:p  \mneq{}  q.  \mforall{}s1:l  \mneq{}  m.
    (p  \mneq{}  l  {}\mRightarrow{}  q  \mneq{}  m  {}\mRightarrow{}  p  I  m  {}\mRightarrow{}  q  I  l  {}\mRightarrow{}  l  \mwedge{}  m  \mneq{}  p  \mvee{}  q)


By

---

Latex:
((Auto  THEN  InstLemma  `projective-plane-axioms`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{})  THEN  Auto)

---

Home Index