---

Step * of Lemma eu-out-refl

∀e:EuclideanPlane. ∀a,b,c:Point.  (out(a bc) ⇒ out(a cb))
BY
{ RepeatFor 5 ((D 0 THENA Auto))
THEN Unfold `eu-out` (-1)
THEN Unfold `eu-out` 0
THEN Auto }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (out(a  bc)  {}\mRightarrow{}  out(a  cb))


By

---

Latex:
RepeatFor  5  ((D  0  THENA  Auto))
THEN  Unfold  `eu-out`  (-1)
THEN  Unfold  `eu-out`  0
THEN  Auto

---

Home Index