---

Step * 12 of Lemma r2-basic-geo-axioms


∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
BY
{ (UnfoldGeoAbbreviations 0 THEN (RWO "r2-be-iff<" 0 THENA Auto)) }

1
∀a,b,x,y,z:ℝ^2.  (r2-left(x;a;b) ⇒ r2-left(y;a;b) ⇒ x_z_y ⇒ r2-left(z;a;b))

---

Latex:

---

Latex:

\mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  leftof  ab)


By

---

Latex:
(UnfoldGeoAbbreviations  0  THEN  (RWO  "r2-be-iff<"  0  THENA  Auto))

---

Home Index