---

Step * 1 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
32. out(b AC)
⊢ AC ≅ XZ
BY
{ ((Assert out(y XZ) BY
          ((InstLemma  `geo-between-out` [⌜g⌝;⌜y⌝;⌜x⌝;⌜z⌝]⋅ THENA Auto)
           THEN ((InstLemma  `geo-between-out` [⌜g⌝;⌜y⌝;⌜z⌝;⌜Z⌝]⋅ THENA Auto)
                 THEN (InstLemma`geo-out_transitivity` [⌜g⌝;⌜y⌝;⌜x⌝;⌜z⌝;⌜X⌝]⋅ THENA Auto)
                 THEN (InstLemma  `geo-between-out` [⌜g⌝;⌜y⌝;⌜x⌝;⌜X⌝]⋅ THENA Auto)
                 THEN InstLemma`geo-out_transitivity` [⌜g⌝;⌜y⌝;⌜z⌝;⌜x⌝;⌜X⌝]⋅
                 THEN EAuto 1)
           THEN InstLemma`geo-out_transitivity` [⌜g⌝;⌜y⌝;⌜Z⌝;⌜z⌝;⌜X⌝]⋅
           THEN EAuto 1))
   THEN InstLemma `geo-out-cong-cong` [⌜g⌝;⌜b⌝;⌜A⌝;⌜C⌝;⌜y⌝;⌜X⌝;⌜Z⌝]⋅
   THEN Auto) }

---

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
32.  out(b  AC)
\mvdash{}  AC  \mcong{}  XZ


By

---

Latex:
((Assert  out(y  XZ)  BY
                ((InstLemma    `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  ((InstLemma    `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  (InstLemma`geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  (InstLemma    `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  InstLemma`geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
                              THEN  EAuto  1)
                  THEN  InstLemma`geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
                  THEN  EAuto  1))
  THEN  InstLemma  `geo-out-cong-cong`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index