---

Step * of Lemma eu-congruent-transitivity

∀e:EuclideanPlane. ∀[a,b,c,d,x,y:Point].  (ab=xy) supposing (cd=xy and ab=cd)
BY
{ (Auto THEN (Assert e ∈ EuclideanPlane BY Auto)) }

1
1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [d] : Point
6. [x] : Point
7. [y] : Point
8. [%] : ab=cd
9. [%1] : cd=xy
10. e ∈ EuclideanPlane
⊢ ab=xy

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,d,x,y:Point].    (ab=xy)  supposing  (cd=xy  and  ab=cd)


By

---

Latex:
(Auto  THEN  (Assert  e  \mmember{}  EuclideanPlane  BY  Auto))

---

Home Index