---

Step * 1 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
30. out(b AC)
⊢ AC ≅ XZ
BY
{ ((Assert out(y XZ) BY
          (((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.  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
30.  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{}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