---

Step * of Lemma use-triangle-axiom1

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

---

Latex:

---

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


By

---

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

---

Home Index