Step
*
of Lemma
parallel-preserves-intersection
∀eu:EuclideanParPlane. ∀l,m,n:Line. ((l \/ m
⇒ (l \/ n ∨ m \/ n))
⇒ (l \/ m ∧ l || n)
⇒ m \/ n)
BY
{ (((Auto THEN D -1) THEN Auto) THEN Unfold `geo-Aparallel` -2 THEN Auto) }
Latex:
Latex:
\mforall{}eu:EuclideanParPlane. \mforall{}l,m,n:Line. ((l \mbackslash{}/ m {}\mRightarrow{} (l \mbackslash{}/ n \mvee{} m \mbackslash{}/ n)) {}\mRightarrow{} (l \mbackslash{}/ m \mwedge{} l || n) {}\mRightarrow{} m \mbackslash{}/ n)
By
Latex:
(((Auto THEN D -1) THEN Auto) THEN Unfold `geo-Aparallel` -2 THEN Auto)
Home
Index