---

Step * of Lemma interior-point-cong-angle-transfer-full

∀g:EuclideanPlane. ∀a,b,c,d,e,f,x,y,z:Point.
  (abc < xyz
  ⇒ def ≅a xyz
  ⇒ d # ef
  ⇒ (∃p,p',d',f':Point. (d'ep ≅a abc ∧ d'_p'_f' ∧ p' ≠ f' ∧ (out(e dd') ∧ out(e ff')) ∧ e_p'_p ∧ (¬d_e_p))))
BY
{ ((Auto THEN Unfold `geo-lt-angle` -3 THEN ExRepD)
   THEN (InstLemma `cong-angle-out-exists-cong3` [⌜g⌝;⌜d⌝;⌜e⌝;⌜f⌝;⌜x'⌝;⌜y⌝;⌜z'⌝]⋅ THENA Auto)
   THEN ExRepD) }

1
.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. ¬out(y xz)
12. p : Point
13. p' : Point
14. x' : Point
15. z' : Point
16. abc ≅a xyp
17. y_p'_p
18. out(y xx')
19. out(y zz')
20. ¬x_y_p
21. x'_p'_z'
22. p' ≠ z'
23. def ≅a xyz
24. d # ef
⊢ def ≅a x'yz'

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. ¬out(y xz)
12. p : Point
13. p' : Point
14. x' : Point
15. z' : Point
16. abc ≅a xyp
17. y_p'_p
18. out(y xx')
19. out(y zz')
20. ¬x_y_p
21. x'_p'_z'
22. p' ≠ z'
23. def ≅a xyz
24. d # ef
25. a' : Point
26. c' : Point
27. out(e a'd)
28. out(e c'f)
29. a'ec' ≅a x'yz'
30. Cong3(a'ec',x'yz')
⊢ ∃p,p',d',f':Point. (d'ep ≅a abc ∧ d'_p'_f' ∧ p' ≠ f' ∧ (out(e dd') ∧ out(e ff')) ∧ e_p'_p ∧ (¬d_e_p))

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f,x,y,z:Point.
    (abc  <  xyz
    {}\mRightarrow{}  def  \mcong{}\msuba{}  xyz
    {}\mRightarrow{}  d  \#  ef
    {}\mRightarrow{}  (\mexists{}p,p',d',f':Point
              (d'ep  \mcong{}\msuba{}  abc  \mwedge{}  d'\_p'\_f'  \mwedge{}  p'  \mneq{}  f'  \mwedge{}  (out(e  dd')  \mwedge{}  out(e  ff'))  \mwedge{}  e\_p'\_p  \mwedge{}  (\mneg{}d\_e\_p))))


By

---

Latex:
((Auto  THEN  Unfold  `geo-lt-angle`  -3  THEN  ExRepD)
  THEN  (InstLemma  `cong-angle-out-exists-cong3`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index