---

Step * 1 1 of Lemma cong-angle-out-exists

.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. ba' ≅ yA
33. bc' ≅ yC
⊢ out(y zC)
BY
{ (InstLemma `geo-out-iff-between1` [⌜g⌝;⌜y⌝;⌜z⌝;⌜C⌝;⌜r2⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  p  :  Point
11.  abc  \mcong{}\msuba{}  xyz
12.  a  \mneq{}  b
13.  c  \mneq{}  b
14.  p  \mneq{}  b
15.  x  \mneq{}  y
16.  z  \mneq{}  y
17.  out(b  aa')
18.  out(b  cc')
19.  a'-p-c'
20.  r1  :  Point
21.  x-y-r1
22.  yr1  \mcong{}  OX
23.  r2  :  Point
24.  z-y-r2
25.  yr2  \mcong{}  OX
26.  A  :  Point
27.  r1-y-A
28.  yA  \mcong{}  ba'
29.  C  :  Point
30.  r2-y-C
31.  yC  \mcong{}  bc'
32.  ba'  \mcong{}  yA
33.  bc'  \mcong{}  yC
\mvdash{}  out(y  zC)


By

---

Latex:
(InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}r2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index