---

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


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Racc
6. a' : Point
7. b' : Point
8. c' : Point
9. ac ≅ a'b'
10. cc ≅ b'c'
11. ca ≅ c'a'
12. b ≡ c
⊢ Ra'b'c'
BY
{ (gEliminatePoints THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  Racc
6.  a'  :  Point
7.  b'  :  Point
8.  c'  :  Point
9.  ac  \00D0  a'b'
10.  cc  \00D0  b'c'
11.  ca  \00D0  c'a'
12.  b  \mequiv{}  c
\mvdash{}  Ra'b'c'


By

---

Latex:
(gEliminatePoints  THEN  Auto)

---

Home Index