---

Step * 1 1 1 of Lemma sup-angles-preserve-congruence

.....antecedent..... 
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
34. Ac' ≅ Xz'
⊢ out(b Aa')
BY
{ (InstLemma `geo-between-out` [⌜e⌝;⌜b⌝;⌜a'⌝;⌜A⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
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  \00D0\msuba{}  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'  \00D0\msuba{}  x1yz'
24.  Cong3(a1bc',x1yz')
25.  A  :  Point
26.  b-a'-A
27.  a'A  \00D0  yx'
28.  X  :  Point
29.  y-x'-X
30.  x'X  \00D0  ba'
31.  a1\_b\_A
32.  x1\_y\_X
33.  bA  \00D0  yX
34.  Ac'  \00D0  Xz'
\mvdash{}  out(b  Aa')


By

---

Latex:
(InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index