---

Step * of Lemma lsep-lt-straight-angle

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (a # bc ⇒ x-y-z ⇒ abc < xyz)
BY
{ (Auto THEN (InstLemma `Euclid-Prop23_half-plane2` [⌜e⌝;⌜y⌝;⌜x⌝;⌜b⌝;⌜c⌝;⌜a⌝]⋅ THENA Auto) THEN ExRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x-y-z
10. x' : Point
11. b' : Point
12. out(y xb')
13. x' leftof b'y
14. x'yb' ≅a abc
⊢ abc < xyz

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-Prop23\_half-plane2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index