---

Step * of Lemma p4eu

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

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

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

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

4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB
11. ac=AC
12. bac = BAC
13. bc=BC
14. abc = ABC
15. bca = BCA
⊢ Cong3(abc,ABC)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index