---

Step * 1 of Lemma congruence-preserves-right-angle


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Rabc
6. a' : Point
7. b' : Point
8. c' : Point
9. ab ≅ a'b'
10. bc ≅ b'c' ∧ ca ≅ c'a'
11. b ≠ c
⊢ Ra'b'c'
BY
{ (gSymmetricPoint ⌜b⌝ ⌜c⌝ `d'⋅ THEN (Assert b' ≠ c' BY Auto) THEN gSymmetricPoint ⌜b'⌝ ⌜c'⌝ `d\''⋅) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Rabc
6. a' : Point
7. b' : Point
8. c' : Point
9. ab ≅ a'b'
10. bc ≅ b'c' ∧ ca ≅ c'a'
11. b ≠ c
12. d : Point
13. c=b=d
14. b' ≠ c'
15. d' : Point
16. c'=b'=d'
⊢ Ra'b'c'

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  Rabc
6.  a'  :  Point
7.  b'  :  Point
8.  c'  :  Point
9.  ab  \00D0  a'b'
10.  bc  \00D0  b'c'  \mwedge{}  ca  \00D0  c'a'
11.  b  \mneq{}  c
\mvdash{}  Ra'b'c'


By

---

Latex:
(gSymmetricPoint  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  `d'\mcdot{}  THEN  (Assert  b'  \mneq{}  c'  BY  Auto)  THEN  gSymmetricPoint  \mkleeneopen{}b'\mkleeneclose{}  \mkleeneopen{}c'\mkleeneclose{}  `d\mbackslash{}''\mcdot{})

---

Home Index