---

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

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

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. a # bc
25. x-y-z
⊢ e ≠ d

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. a # bc
25. x-y-z
26. ∃x',b':Point. (out(e db') ∧ x' # eb' ∧ x'eb' ≅a abc)
⊢ abc < def

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Unfold  `geo-lt-angle`  -4  THEN  ExRepD)
  THEN  (InstLemma    `Euclid-Prop23`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index