---

Step * of Lemma geo-reflected-right-triangles-congruent

∀e:BasicGeometry. ∀a,b,c,d:Point.  (a # bc ⇒ Rcba ⇒ a=b=d ⇒ Cong3(abc,dbc))
BY
{ (Auto THEN (Assert Rcbd BY (Unfold `right-angle` -2 THEN InstHyp [⌜d⌝] (-2)⋅ THEN EAuto 1))) }

1
.....aux..... 
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. ∀c':Point. (c'=b=a ⇒ ca ≅ cc')
8. a=b=d
9. ca ≅ cd
⊢ Rcbd

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. Rcba
8. a=b=d
9. Rcbd
⊢ Cong3(abc,dbc)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (a  \#  bc  {}\mRightarrow{}  Rcba  {}\mRightarrow{}  a=b=d  {}\mRightarrow{}  Cong3(abc,dbc))


By

---

Latex:
(Auto  THEN  (Assert  Rcbd  BY  (Unfold  `right-angle`  -2  THEN  InstHyp  [\mkleeneopen{}d\mkleeneclose{}]  (-2)\mcdot{}  THEN  EAuto  1)))

---

Home Index