---

Step * of Lemma congruence-preserves-right-angle2

∀e:BasicGeometry. ∀a,b,c:Point.  (Rabc ⇒ (∀a',b',c':Point.  (abc ≅a a'b'c' ⇒ Ra'b'c')))
BY
{ (Auto
   THEN (InstLemma `cong-angle-out-exists-cong3` [⌜e⌝;⌜a'⌝;⌜b'⌝;⌜c'⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA EAuto 1)
   THEN ExRepD
   THEN (InstLemma `congruence-preserves-right-angle` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
   THEN ((InstHyp [⌜a'@0⌝;⌜b'⌝;⌜c'@0⌝] (-1)⋅ THEN Auto) THENA ((D 0 THEN Auto) THEN D 15 THEN EAuto 1))) }

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. abc ≅a a'b'c'
10. a'@0 : Point
11. c'@0 : Point
12. out(b' a'@0a')
13. out(b' c'@0c')
14. a'@0b'c'@0 ≅a abc
15. Cong3(a'@0b'c'@0,abc)
16. ∀a',b',c':Point.  (Cong3(abc,a'b'c') ⇒ Ra'b'c')
17. Ra'@0b'c'@0
⊢ Ra'b'c'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (Rabc  {}\mRightarrow{}  (\mforall{}a',b',c':Point.    (abc  \mcong{}\msuba{}  a'b'c'  {}\mRightarrow{}  Ra'b'c')))


By

---

Latex:
(Auto
  THEN  (InstLemma  `cong-angle-out-exists-cong3`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  ExRepD
  THEN  (InstLemma  `congruence-preserves-right-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstHyp  [\mkleeneopen{}a'@0\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'@0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
              THENA  ((D  0  THEN  Auto)  THEN  D  15  THEN  EAuto  1)
              ))

---

Home Index