---

Step * of Lemma cong-angle-out-exists

∀g:EuclideanPlane. ∀a,b,c,x,y,z,a',c',p:Point.
  (abc ≅a xyz
  ⇒ a ≠ b
  ⇒ c ≠ b
  ⇒ p ≠ b
  ⇒ x ≠ y
  ⇒ z ≠ y
  ⇒ ((out(b aa') ∧ out(b cc')) ∧ a'-p-c')
  ⇒ (∃x',z',p':Point
       (((x'-p'-z' ∧ Cong3(a'bc',x'yz')) ∧ out(y xx') ∧ out(y zz'))
       ∧ (x'p' ≅ a'p ∧ p'z' ≅ pc')
       ∧ bp ≅ yp'
       ∧ x'yp' ≅a a'bp)))
BY
{ ((UnivCD THENW Auto)
   THEN (gProperProlong ⌜x⌝⌜y⌝`r1'⌜O⌝⌜X⌝⋅ THENA Auto)
   THEN ((gProperProlong ⌜z⌝⌜y⌝`r2'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜r1⌝⌜y⌝`A'⌜b⌝⌜a'⌝⋅ THENA Auto)
   THEN (gProperProlong ⌜r2⌝⌜y⌝`C'⌜b⌝⌜c'⌝⋅ THENA Auto)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A ∧ yA ≅ ba'
28. C : Point
29. r2-y-C ∧ yC ≅ bc'
⊢ ∃x',z',p':Point
   (((x'-p'-z' ∧ Cong3(a'bc',x'yz')) ∧ out(y xx') ∧ out(y zz')) ∧ (x'p' ≅ a'p ∧ p'z' ≅ pc') ∧ bp ≅ yp' ∧ x'yp' ≅a a'bp)

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y,z,a',c',p:Point.
    (abc  \mcong{}\msuba{}  xyz
    {}\mRightarrow{}  a  \mneq{}  b
    {}\mRightarrow{}  c  \mneq{}  b
    {}\mRightarrow{}  p  \mneq{}  b
    {}\mRightarrow{}  x  \mneq{}  y
    {}\mRightarrow{}  z  \mneq{}  y
    {}\mRightarrow{}  ((out(b  aa')  \mwedge{}  out(b  cc'))  \mwedge{}  a'-p-c')
    {}\mRightarrow{}  (\mexists{}x',z',p':Point
              (((x'-p'-z'  \mwedge{}  Cong3(a'bc',x'yz'))  \mwedge{}  out(y  xx')  \mwedge{}  out(y  zz'))
              \mwedge{}  (x'p'  \mcong{}  a'p  \mwedge{}  p'z'  \mcong{}  pc')
              \mwedge{}  bp  \mcong{}  yp'
              \mwedge{}  x'yp'  \mcong{}\msuba{}  a'bp)))


By

---

Latex:
((UnivCD  THENW  Auto)
  THEN  (gProperProlong  \mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`r1'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((gProperProlong  \mkleeneopen{}z\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`r2'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}r1\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`A'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong  \mkleeneopen{}r2\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}`C'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index