---

Step * of Lemma eqtri_wf

∀[e:EuclideanPlane]. ∀[a:Point]. ∀[b:{b:Point| a ≠ b} ].
  (Δ(a;b) ∈ {c:Point| ((cb ≅ ab ∧ ca ≅ ba) ∧ ca ≅ cb) ∧ c leftof ab} )
BY
{ (Auto THEN (Subst' Δ(a;b) ~ TERMOF{Euclid-Prop1-left:o, 1:l, i:l} e a b 0 THENA Computation) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Subst'  \mDelta{}(a;b)  \msim{}  TERMOF\{Euclid-Prop1-left:o,  1:l,  i:l\}  e  a  b  0  THENA  Computation)
  THEN  Auto)

---

Home Index