---

Step * of Lemma zero-angles-congruent2

∀g:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (out(b ac) ⇒ out(y xz) ⇒ abc ≅a xyz)
BY
{ (((Auto THEN Unfold `geo-cong-angle` 0) THEN GenRepD THEN Auto)
   THEN ((gProperProlong  ⌜b⌝⌜a⌝`A'⌜y⌝⌜x⌝⋅ THENA Auto) THEN (Assert b ≠ c BY Auto) THEN (Assert y ≠ z BY Auto))
   THEN (gProperProlong  ⌜b⌝⌜c⌝`C'⌜y⌝⌜z⌝⋅ THENA Auto)
   THEN (gProperProlong  ⌜y⌝⌜x⌝`X'⌜a⌝⌜b⌝⋅ THENA Auto)
   THEN (gProperProlong  ⌜y⌝⌜z⌝`Z'⌜b⌝⌜c⌝⋅ THENA Auto)
   THEN InstConcl [⌜A⌝;⌜C⌝;⌜X⌝;⌜Z⌝]⋅
   THEN Auto) }

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
⊢ AC ≅ XZ

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (out(b  ac)  {}\mRightarrow{}  out(y  xz)  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz)


By

---

Latex:
(((Auto  THEN  Unfold  `geo-cong-angle`  0)  THEN  GenRepD  THEN  Auto)
  THEN  ((gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (Assert  b  \mneq{}  c  BY
                                      Auto)
              THEN  (Assert  y  \mneq{}  z  BY
                                      Auto))
  THEN  (gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`C'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong    \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}`X'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong    \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}`Z'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index