---

Step * 1 of Lemma zero-angles-congruent


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. y ≠ x
10. b_a_c
11. y_x_z
12. A : Point
13. b-a-A
14. aA ≅ yx
15. b ≠ c
16. y ≠ z
17. C : Point
18. b-c-C
19. cC ≅ yz
20. X : Point
21. y-x-X
22. xX ≅ ab
23. Z : Point
24. y-z-Z
25. zZ ≅ bc
26. b_a_A
27. b_c_C
28. y_x_X
29. y_z_Z
30. bA ≅ yX
31. bC ≅ yZ
⊢ AC ≅ XZ
BY
{ (Assert out(b AC) BY
         ((InstLemma  `geo-between-out` [⌜g⌝;⌜b⌝;⌜a⌝;⌜c⌝]⋅ THENA Auto)
          THEN ((InstLemma  `geo-between-out` [⌜g⌝;⌜b⌝;⌜c⌝;⌜C⌝]⋅ THENA Auto)
                THEN (InstLemma`geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜C⌝]⋅ THENA Auto)
                THEN (InstLemma  `geo-between-out` [⌜g⌝;⌜b⌝;⌜a⌝;⌜A⌝]⋅ THENA Auto)
                THEN (InstLemma`geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜A⌝]⋅ THENA EAuto 1))
          THEN InstLemma`geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜C⌝;⌜c⌝;⌜A⌝]⋅
          THEN EAuto 1)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. y ≠ x
10. b_a_c
11. y_x_z
12. A : Point
13. b-a-A
14. aA ≅ yx
15. b ≠ c
16. y ≠ z
17. C : Point
18. b-c-C
19. cC ≅ yz
20. X : Point
21. y-x-X
22. xX ≅ ab
23. Z : Point
24. y-z-Z
25. zZ ≅ bc
26. b_a_A
27. b_c_C
28. y_x_X
29. y_z_Z
30. bA ≅ yX
31. bC ≅ yZ
32. out(b AC)
⊢ AC ≅ XZ

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  b  \mneq{}  a
9.  y  \mneq{}  x
10.  b\_a\_c
11.  y\_x\_z
12.  A  :  Point
13.  b-a-A
14.  aA  \mcong{}  yx
15.  b  \mneq{}  c
16.  y  \mneq{}  z
17.  C  :  Point
18.  b-c-C
19.  cC  \mcong{}  yz
20.  X  :  Point
21.  y-x-X
22.  xX  \mcong{}  ab
23.  Z  :  Point
24.  y-z-Z
25.  zZ  \mcong{}  bc
26.  b\_a\_A
27.  b\_c\_C
28.  y\_x\_X
29.  y\_z\_Z
30.  bA  \mcong{}  yX
31.  bC  \mcong{}  yZ
\mvdash{}  AC  \mcong{}  XZ


By

---

Latex:
(Assert  out(b  AC)  BY
              ((InstLemma    `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ((InstLemma    `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstLemma`geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstLemma    `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstLemma`geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  EAuto  1))
                THEN  InstLemma`geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
                THEN  EAuto  1))

---

Home Index