---

Step * of Lemma cong-angle-out-exists2

∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.
  (abc ≅a xyz
  ⇒ a ≠ b
  ⇒ c ≠ b
  ⇒ x ≠ y
  ⇒ z ≠ y
  ⇒ (∃a',c',x',z':Point. (out(b a'a) ∧ out(b c'c) ∧ out(y x'x) ∧ out(y z'z) ∧ a'bc' ≅a x'yz')))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `geo-cong-angle` 8
   THEN ExRepD
   THEN (Assert ⌜out(b aa')⌝⋅ THEN EAuto 1)
   THEN Assert ⌜out(b a'a)⌝⋅
   THEN EAuto 1) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a ≠ b
9. b ≠ c
10. x ≠ y
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. b_a_a'
17. b_c_c'
18. y_x_x'
19. y_z_z'
20. ba' ≅ yx'
21. bc' ≅ yz'
22. a'c' ≅ x'z'
23. a ≠ b
24. c ≠ b
25. x ≠ y
26. z ≠ y
27. out(b aa')
28. out(b a'a)
⊢ ∃a',c',x',z':Point. (out(b a'a) ∧ out(b c'c) ∧ out(y x'x) ∧ out(y z'z) ∧ a'bc' ≅a x'yz')

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (abc  \mcong{}\msuba{}  xyz
    {}\mRightarrow{}  a  \mneq{}  b
    {}\mRightarrow{}  c  \mneq{}  b
    {}\mRightarrow{}  x  \mneq{}  y
    {}\mRightarrow{}  z  \mneq{}  y
    {}\mRightarrow{}  (\mexists{}a',c',x',z':Point.  (out(b  a'a)  \mwedge{}  out(b  c'c)  \mwedge{}  out(y  x'x)  \mwedge{}  out(y  z'z)  \mwedge{}  a'bc'  \mcong{}\msuba{}  x'yz')))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `geo-cong-angle`  8
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}out(b  aa')\mkleeneclose{}\mcdot{}  THEN  EAuto  1)
  THEN  Assert  \mkleeneopen{}out(b  a'a)\mkleeneclose{}\mcdot{}
  THEN  EAuto  1)

---

Home Index