---

Step * of Lemma geo-cong-angle-symm3

∀e:BasicGeometry. ∀x,y,z,a,b,c:Point.  (xyz ≅a abc ⇒ zyx ≅a cba)
BY
{ (Auto THEN Unfold `geo-cong-angle` 8 THEN (Unfold `geo-cong-angle` 0 THEN ExRepD) THEN D 0) }

1
1. e : BasicGeometry
2. x : Point
3. y : Point
4. z : Point
5. a : Point
6. b : Point
7. c : Point
8. x ≠ y
9. y ≠ z
10. a ≠ b
11. b ≠ c
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. y_x_a'
17. y_z_c'
18. b_a_x'
19. b_c_z'
20. ya' ≅ bx'
21. yc' ≅ bz'
22. a'c' ≅ x'z'
⊢ ((z ≠ y ∧ y ≠ x) ∧ c ≠ b) ∧ b ≠ a

2
1. e : BasicGeometry
2. x : Point
3. y : Point
4. z : Point
5. a : Point
6. b : Point
7. c : Point
8. x ≠ y
9. y ≠ z
10. a ≠ b
11. b ≠ c
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. y_x_a'
17. y_z_c'
18. b_a_x'
19. b_c_z'
20. ya' ≅ bx'
21. yc' ≅ bz'
22. a'c' ≅ x'z'
⊢ ∃a',c',x',z':Point. (y_z_a' ∧ y_x_c' ∧ b_c_x' ∧ b_a_z' ∧ ya' ≅ bx' ∧ yc' ≅ bz' ∧ a'c' ≅ x'z')

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}x,y,z,a,b,c:Point.    (xyz  \mcong{}\msuba{}  abc  {}\mRightarrow{}  zyx  \mcong{}\msuba{}  cba)


By

---

Latex:
(Auto  THEN  Unfold  `geo-cong-angle`  8  THEN  (Unfold  `geo-cong-angle`  0  THEN  ExRepD)  THEN  D  0)

---

Home Index