---

Step * of Lemma sup-angles-preserve-congruence

∀e:HeytingGeometry. ∀a,b,c,x,y,z,a',x':Point.  ((abc ≅a xyz ∧ a # bc ∧ x # yz) ⇒ a-b-a' ⇒ x-y-x' ⇒ a'bc ≅a x'yz)
BY
{ ((Auto THEN (FLemma `cong-angle-out-exists3` [10] THEN Auto) THEN ExRepD)
   THEN ((gProperProlong ⌜b⌝⌜a'⌝`A'⌜y⌝⌜x'⌝⋅ THEN Auto) THEN gProperProlong ⌜y⌝⌜x'⌝`X'⌜b⌝⌜a'⌝⋅ THEN Auto)
   THEN ((InstLemma `geo-bet-out-out-bet` [⌜e⌝;⌜b⌝;⌜a⌝;⌜a1⌝;⌜a'⌝;⌜A⌝]⋅ THENA EAuto 1)
         THEN (InstLemma `geo-bet-out-out-bet` [⌜e⌝;⌜y⌝;⌜x⌝;⌜x1⌝;⌜x'⌝;⌜X⌝]⋅ THENA EAuto 1)
         )
   THEN (Assert bA ≅ yX BY
               ((D 26 THEN FLemma `geo-add-length-between` [26] THEN Auto)
                THEN D 31
                THEN FLemma `geo-add-length-between` [31]
                THEN Auto))) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. x' : Point
10. abc ≅a xyz
11. a # bc
12. x # yz
13. a-b-a'
14. x-y-x'
15. a1 : Point
16. c' : Point
17. x1 : Point
18. z' : Point
19. out(b a1a)
20. out(b c'c)
21. out(y x1x)
22. out(y z'z)
23. a1bc' ≅a x1yz'
24. Cong3(a1bc',x1yz')
25. A : Point
26. b-a'-A
27. a'A ≅ yx'
28. X : Point
29. y-x'-X
30. x'X ≅ ba'
31. a1_b_A
32. x1_y_X
33. bA ≅ yX
⊢ a'bc ≅a x'yz

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,x,y,z,a',x':Point.
    ((abc  \00D0\msuba{}  xyz  \mwedge{}  a  \#  bc  \mwedge{}  x  \#  yz)  {}\mRightarrow{}  a-b-a'  {}\mRightarrow{}  x-y-x'  {}\mRightarrow{}  a'bc  \00D0\msuba{}  x'yz)


By

---

Latex:
((Auto  THEN  (FLemma  `cong-angle-out-exists3`  [10]  THEN  Auto)  THEN  ExRepD)
  THEN  ((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`A'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}\mcdot{}  THEN  Auto)
              THEN  gProperProlong  \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}`X'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mcdot{}
              THEN  Auto)
  THEN  ((InstLemma  `geo-bet-out-out-bet`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
              THEN  (InstLemma  `geo-bet-out-out-bet`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
              )
  THEN  (Assert  bA  \00D0  yX  BY
                          ((D  26  THEN  FLemma  `geo-add-length-between`  [26]  THEN  Auto)
                            THEN  D  31
                            THEN  FLemma  `geo-add-length-between`  [31]
                            THEN  Auto)))

---

Home Index