---

Step * 1 of Lemma right-angle-SAS


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. Rabc
9. a # b
10. b # c
11. Rxyz
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
⊢ ac ≅ xz
BY
{ (((gProperProlong  ⌜c⌝⌜b⌝`c\''⌜c⌝⌜b⌝⋅ THEN Auto) THEN gProperProlong  ⌜z⌝⌜y⌝`z\''⌜z⌝⌜y⌝⋅ THEN Auto)
   THEN (Duplicate (8) ⋅ THEN Duplicate (11))
   THEN Unfold `right-angle` 8
   THEN Unfold `right-angle` 11) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
9. a # b
10. b # c
11. ∀c':Point. (c'=y=z ⇒ xz ≅ xc')
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
16. c' : Point
17. c-b-c'
18. bc' ≅ cb
19. z' : Point
20. z-y-z'
21. yz' ≅ zy
22. Rabc
23. Rxyz
⊢ ac ≅ xz

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  Rabc
9.  a  \#  b
10.  b  \#  c
11.  Rxyz
12.  x  \#  y
13.  y  \#  z
14.  ab  \mcong{}  xy
15.  bc  \mcong{}  yz
\mvdash{}  ac  \mcong{}  xz


By

---

Latex:
(((gProperProlong    \mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c\mbackslash{}''\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  gProperProlong    \mkleeneopen{}z\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`z\mbackslash{}''\mkleeneopen{}z\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Duplicate  (8)  \mcdot{}  THEN  Duplicate  (11))
  THEN  Unfold  `right-angle`  8
  THEN  Unfold  `right-angle`  11)

---

Home Index