---

Step * of Lemma between-preserves-left-6

No Annotations
∀e:EuclideanPlane. ∀A,B,C,V:Point.  (C leftof AB ⇒ B # V ⇒ B(VAB) ⇒ C leftof VB)
BY
{ (Auto THEN GeometryMasterTactic true 2) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C,V:Point.    (C  leftof  AB  {}\mRightarrow{}  B  \#  V  {}\mRightarrow{}  B(VAB)  {}\mRightarrow{}  C  leftof  VB)


By

---

Latex:
(Auto  THEN  GeometryMasterTactic  true  2)

---

Home Index