---

Step * of Lemma Euclid-Prop4

∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
  ((Triangle(a;b;c) ∧ Triangle(A;B;C))
  ⇒ (ab ≅ AB ∧ ac ≅ AC ∧ bac ≅a BAC)
  ⇒ (bc ≅ BC ∧ abc ≅a ABC ∧ bca ≅a BCA ∧ Cong3(abc,ABC)))
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 ≅a 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 ≅a BAC
13. bc ≅ BC
⊢ abc ≅a 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 ≅a BAC
13. bc ≅ BC
14. abc ≅a ABC
⊢ bca ≅a 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 ≅a BAC
13. bc ≅ BC
14. abc ≅a ABC
15. bca ≅a BCA
⊢ Cong3(abc,ABC)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index