---

Step * of Lemma p4-triangles

∀e:HeytingGeometry. ∀a,b,c,x,y,z:Point.
  (a # bc ⇒ x # yz ⇒ ab ≅ xy ⇒ ac ≅ xz ⇒ bac ≅a yxz ⇒ ((bc ≅ yz ∧ Cong3(abc,xyz)) ∧ abc ≅a xyz ∧ bca ≅a yzx))
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. ab ≅ xy
11. ac ≅ xz
12. bac ≅a yxz
⊢ bc ≅ yz

2
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. ab ≅ xy
11. ac ≅ xz
12. bac ≅a yxz
13. bc ≅ yz
⊢ Cong3(abc,xyz)

3
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. ab ≅ xy
11. ac ≅ xz
12. bac ≅a yxz
13. bc ≅ yz
14. Cong3(abc,xyz)
⊢ abc ≅a xyz

4
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. ab ≅ xy
11. ac ≅ xz
12. bac ≅a yxz
13. bc ≅ yz
14. Cong3(abc,xyz)
15. abc ≅a xyz
⊢ bca ≅a yzx

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (a  \#  bc
    {}\mRightarrow{}  x  \#  yz
    {}\mRightarrow{}  ab  \mcong{}  xy
    {}\mRightarrow{}  ac  \mcong{}  xz
    {}\mRightarrow{}  bac  \mcong{}\msuba{}  yxz
    {}\mRightarrow{}  ((bc  \mcong{}  yz  \mwedge{}  Cong3(abc,xyz))  \mwedge{}  abc  \mcong{}\msuba{}  xyz  \mwedge{}  bca  \mcong{}\msuba{}  yzx))


By

---

Latex:
Auto

---

Home Index