---

Step * of Lemma geo-lt-angle-in-half-plane-implies-left2

∀e:EuclideanPlane. ∀w,x,y,z:Point.  (xyz < wyz ⇒ w leftof zy ⇒ x leftof zy ⇒ w leftof xy)
BY
{ (Auto THEN (Assert xyz < zyw BY (FLemma `geo-lt-angle-symm` [-3] THEN Auto))) }

1
1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof zy
8. x leftof zy
9. xyz < zyw
⊢ w leftof xy

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}w,x,y,z:Point.    (xyz  <  wyz  {}\mRightarrow{}  w  leftof  zy  {}\mRightarrow{}  x  leftof  zy  {}\mRightarrow{}  w  leftof  xy)


By

---

Latex:
(Auto  THEN  (Assert  xyz  <  zyw  BY  (FLemma  `geo-lt-angle-symm`  [-3]  THEN  Auto)))

---

Home Index