---

Step * of Lemma Euclid-Prop1-left-ext

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} .  (∃c:Point [(((cb ≅ ab ∧ ca ≅ ba) ∧ ca ≅ cb) ∧ c leftof ab)])
BY
{ Extract of Obid: Euclid-Prop1-left
  not unfolding  geo-CCL
  finishing with (Fold  `eqtri` 0 THEN Auto)
  normalizes to:
  
  λe,a,b. Δ(a;b) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .
    (\mexists{}c:Point  [(((cb  \mcong{}  ab  \mwedge{}  ca  \mcong{}  ba)  \mwedge{}  ca  \mcong{}  cb)  \mwedge{}  c  leftof  ab)])


By

---

Latex:
Extract  of  Obid:  Euclid-Prop1-left
not  unfolding    geo-CCL
finishing  with  (Fold    `eqtri`  0  THEN  Auto)
normalizes  to:

\mlambda{}e,a,b.  \mDelta{}(a;b)

---

Home Index