Step
*
of Lemma
between-preserves-left-2
∀e:EuclideanPlane. ∀A,B,C,V:Point.  (C leftof AB 
⇒ A ≠ V 
⇒ A_V_B 
⇒ C leftof AV)
BY
{ (Auto THEN GeometryMasterTactic true 2) }
Latex:
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C,V:Point.    (C  leftof  AB  {}\mRightarrow{}  A  \mneq{}  V  {}\mRightarrow{}  A\_V\_B  {}\mRightarrow{}  C  leftof  AV)
By
Latex:
(Auto  THEN  GeometryMasterTactic  true  2)
Home
Index