---

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

.....antecedent..... 
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ out(b Aa)
BY
{ ((InstLemma `geo-between-out` [⌜e⌝;⌜b⌝;⌜a'⌝;⌜A⌝]⋅ THEN Auto)
   THEN InstLemma `geo-out_transitivity` [⌜e⌝;⌜b⌝;⌜a⌝;⌜a'⌝;⌜A⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  b  \mneq{}  a
9.  b  \mneq{}  c
10.  y  \mneq{}  x
11.  y  \mneq{}  z
12.  a'  :  Point
13.  c'  :  Point
14.  x'  :  Point
15.  z'  :  Point
16.  out(b  a'a)
17.  out(b  c'c)
18.  out(y  x'x)
19.  out(y  z'z)
20.  a'  \mneq{}  b
21.  b  \mneq{}  c'
22.  x'  \mneq{}  y
23.  y  \mneq{}  z'
24.  A  :  Point
25.  C  :  Point
26.  X  :  Point
27.  Z  :  Point
28.  b\_a'\_A
29.  b\_c'\_C
30.  y\_x'\_X
31.  y\_z'\_Z
32.  bA  \mcong{}  yX
33.  bC  \mcong{}  yZ
34.  AC  \mcong{}  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  Auto)
  THEN  InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index