---

Step * of Lemma euclid-Prop3

∀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
{ (Auto THEN (Assert A ≠ B ∧ C1 ≠ C2 BY (DSetVars THEN Unhide THEN Auto))) }

1
1. e : EuclideanPlane
2. A : Point
3. B : {B:Point| A ≠ B} 
4. C1 : Point
5. C2 : {C2:Point| C1 ≠ C2} 
6. |C1C2| < |AB|
7. A ≠ B ∧ C1 ≠ C2
⊢ ∃E:{Point| (A_E_B ∧ AE ≅ 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  \00D0  C1C2)\}))


By

---

Latex:
(Auto  THEN  (Assert  A  \mneq{}  B  \mwedge{}  C1  \mneq{}  C2  BY  (DSetVars  THEN  Unhide  THEN  Auto)))

---

Home Index