---

Step * 1 of Lemma zero-angles-congruent2


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. out(b ac)
9. out(y xz)
10. A : Point
11. b-a-A
12. aA ≅ yx
13. b ≠ c
14. y ≠ z
15. C : Point
16. b-c-C
17. cC ≅ yz
18. X : Point
19. y-x-X
20. xX ≅ ab
21. Z : Point
22. y-z-Z
23. zZ ≅ bc
24. b_a_A
25. b_c_C
26. y_x_X
27. y_z_Z
28. bA ≅ yX
29. bC ≅ yZ
⊢ AC ≅ XZ
BY
{ (Assert out(b AC) BY
         (((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. out(b ac)
9. out(y xz)
10. A : Point
11. b-a-A
12. aA ≅ yx
13. b ≠ c
14. y ≠ z
15. C : Point
16. b-c-C
17. cC ≅ yz
18. X : Point
19. y-x-X
20. xX ≅ ab
21. Z : Point
22. y-z-Z
23. zZ ≅ bc
24. b_a_A
25. b_c_C
26. y_x_X
27. y_z_Z
28. bA ≅ yX
29. bC ≅ yZ
30. 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.  out(b  ac)
9.  out(y  xz)
10.  A  :  Point
11.  b-a-A
12.  aA  \mcong{}  yx
13.  b  \mneq{}  c
14.  y  \mneq{}  z
15.  C  :  Point
16.  b-c-C
17.  cC  \mcong{}  yz
18.  X  :  Point
19.  y-x-X
20.  xX  \mcong{}  ab
21.  Z  :  Point
22.  y-z-Z
23.  zZ  \mcong{}  bc
24.  b\_a\_A
25.  b\_c\_C
26.  y\_x\_X
27.  y\_z\_Z
28.  bA  \mcong{}  yX
29.  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{}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