---

Step * of Lemma eu-sas

∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
  ((ab=AB ∧ ac=AC) ∧ bac = BAC) ⇒ bc=BC supposing Triangle(a;b;c) ∧ Triangle(A;B;C)
BY
{ Auto }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. A : Point@i
6. B : Point@i
7. C : Point@i
8. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB@i
11. ac=AC@i
12. bac = BAC@i
⊢ bc=BC

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,A,B,C:Point.
    ((ab=AB  \mwedge{}  ac=AC)  \mwedge{}  bac  =  BAC)  {}\mRightarrow{}  bc=BC  supposing  Triangle(a;b;c)  \mwedge{}  Triangle(A;B;C)


By

---

Latex:
Auto

---

Home Index