---

Step * of Lemma euclid-Prop3-ext

∀e:EuclideanPlane. ∀A:Point. ∀B:{B:Point| A ≠ B} . ∀C1:Point. ∀C2:{C2:Point| C1 ≠ C2} .
  (|C1C2| < |AB| ⇒ (∃E:Point [(A_E_B ∧ AE ≅ C1C2)]))
BY
{ Extract of Obid: euclid-Prop3
  not unfolding  geo-extend
  finishing with Auto
  normalizes to:
  
  λe,A,B,C1,C2,%. extend extend BA by C1C2A by C1C2 }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A:Point.  \mforall{}B:\{B:Point|  A  \mneq{}  B\}  .  \mforall{}C1:Point.  \mforall{}C2:\{C2:Point|  C1  \mneq{}  C2\}  .
    (|C1C2|  <  |AB|  {}\mRightarrow{}  (\mexists{}E:Point  [(A\_E\_B  \mwedge{}  AE  \mcong{}  C1C2)]))


By

---

Latex:
Extract  of  Obid:  euclid-Prop3
not  unfolding    geo-extend
finishing  with  Auto
normalizes  to:

\mlambda{}e,A,B,C1,C2,\%.  extend  extend  BA  by  C1C2A  by  C1C2

---

Home Index