---

Step * of Lemma geo-cong-angle-preserves-lt-angle2

∀g:EuclideanPlane. ∀a,b,c,d,e,f,x,y,z:Point.  (def ≅a xyz ⇒ abc < xyz ⇒ d # ef ⇒ abc < def)
BY
{ ((Auto
    THEN (InstLemma `interior-point-cong-angle-transfer-full` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜e⌝;⌜f⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THENA Auto)
    THEN ExRepD)
   THEN Unfold `geo-lt-angle` 0
   ) }

1
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. def ≅a xyz
12. abc < xyz
13. d # ef
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. d'ep ≅a abc
19. d'_p'_f'
20. p' ≠ f'
21. out(e dd')
22. out(e ff')
23. e_p'_p
24. ¬d_e_p
⊢ (¬out(e df)) ∧ (∃p,p',x',z':Point. (abc ≅a dep ∧ e_p'_p ∧ (out(e dx') ∧ out(e fz')) ∧ (¬d_e_p) ∧ x'_p'_z' ∧ p' ≠ z'))

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f,x,y,z:Point.    (def  \mcong{}\msuba{}  xyz  {}\mRightarrow{}  abc  <  xyz  {}\mRightarrow{}  d  \#  ef  {}\mRightarrow{}  abc  <  def)


By

---

Latex:
((Auto
    THEN  (InstLemma  `interior-point-cong-angle-transfer-full`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}
                ]\mcdot{}
                THENA  Auto
                )
    THEN  ExRepD)
  THEN  Unfold  `geo-lt-angle`  0
  )

---

Home Index