---

Step * 1 of Lemma straight-angles-not-lt


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a-b-c
9. x-y-z
⊢ ¬abc < xyz
BY
{ ((D 0 THENA Auto) THEN Unfold `geo-lt-angle` -1) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a-b-c
9. x-y-z
10. (¬out(y xz))
∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ y_p'_p ∧ (out(y xx') ∧ out(y zz')) ∧ (¬x_y_p) ∧ x'_p'_z' ∧ p' ≠ z'))
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a-b-c
9.  x-y-z
\mvdash{}  \mneg{}abc  <  xyz


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `geo-lt-angle`  -1)

---

Home Index