Step
*
of Lemma
basic-projective-plane-axioms
∀g:BasicProjectivePlane. ∀m,l:Line. ∀p,q:Point. (p I l
⇒ q I l
⇒ p I m
⇒ q I m
⇒ (¬((¬p ≡ q) ∧ (¬l ≡ m))))
BY
{ (Auto THEN D 1 THEN Auto) }
Latex:
Latex:
\mforall{}g:BasicProjectivePlane. \mforall{}m,l:Line. \mforall{}p,q:Point.
(p I l {}\mRightarrow{} q I l {}\mRightarrow{} p I m {}\mRightarrow{} q I m {}\mRightarrow{} (\mneg{}((\mneg{}p \mequiv{} q) \mwedge{} (\mneg{}l \mequiv{} m))))
By
Latex:
(Auto THEN D 1 THEN Auto)
Home
Index