---

Step * of Lemma hypotenuse-leg-congruence

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  (Rabc ⇒ Rxyz ⇒ ac ≅ xz ⇒ ab ≅ xy ⇒ a ≠ b ⇒ x ≠ y ⇒ b ≠ c ⇒ y ≠ z ⇒ bc ≅ yz)
BY
{ (Auto
   THEN (gProperProlong ⌜a⌝⌜b⌝`b1'⌜a⌝⌜b⌝⋅ THENA Auto)
   THEN (gProperProlong ⌜x⌝⌜y⌝`y1'⌜x⌝⌜y⌝⋅ THENA Auto)
   THEN ExRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. Rabc
9. Rxyz
10. ac ≅ xz
11. ab ≅ xy
12. a ≠ b
13. x ≠ y
14. b ≠ c
15. y ≠ z
16. b1 : Point
17. a-b-b1
18. bb1 ≅ ab
19. y1 : Point
20. x-y-y1
21. yy1 ≅ xy
⊢ bc ≅ yz

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (Rabc  {}\mRightarrow{}  Rxyz  {}\mRightarrow{}  ac  \mcong{}  xz  {}\mRightarrow{}  ab  \mcong{}  xy  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  x  \mneq{}  y  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  y  \mneq{}  z  {}\mRightarrow{}  bc  \mcong{}  yz)


By

---

Latex:
(Auto
  THEN  (gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`b1'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong  \mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`y1'\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index