---

Step * of Lemma geo-lt-angle-in-half-plane-point-exists

∀e:EuclideanPlane. ∀w,x,y,z:Point.  (xyz < wyz ⇒ w leftof yz ⇒ x leftof yz ⇒ (∃q:Point. (w-q-z ∧ out(y qx))))
BY
{ (Auto
   THEN (InstLemma `geo-lt-angle-in-half-plane-implies-left` [⌜e⌝;⌜w⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THEN Auto)
   THEN (InstLemma `use-plane-sep_strict` [⌜e⌝;⌜y⌝;⌜x⌝;⌜w⌝;⌜z⌝]⋅ THENA Auto)) }

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

2
1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof yz
8. x leftof yz
9. w leftof yx
10. ∃x@0:Point. (Colinear(y;x;x@0) ∧ w-x@0-z)
⊢ ∃q:Point. (w-q-z ∧ out(y qx))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}w,x,y,z:Point.
    (xyz  <  wyz  {}\mRightarrow{}  w  leftof  yz  {}\mRightarrow{}  x  leftof  yz  {}\mRightarrow{}  (\mexists{}q:Point.  (w-q-z  \mwedge{}  out(y  qx))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-lt-angle-in-half-plane-implies-left`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `use-plane-sep\_strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index