---

Step * of Lemma segment-density-strict

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} .  (∃x:{Point| a-x-b})
BY
{ (InstLemma `Euclid-Prop10` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .    (\mexists{}x:\{Point|  a-x-b\})


By

---

Latex:
(InstLemma  `Euclid-Prop10`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))  THEN  Auto)

---

Home Index