---

Step * of Lemma geo-lt-angle-left

∀e:EuclideanPlane. ∀a,b,x,y:Point.  (x leftof ab ⇒ y leftof ab ⇒ y leftof xa ⇒ yab < xab)
BY
{ (Auto THEN (InstLemma `use-plane-sep_strict` [⌜e⌝;⌜a⌝;⌜y⌝;⌜x⌝;⌜b⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ab
8. y leftof xa
⊢ x leftof ay

2
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ab
8. y leftof xa
⊢ b leftof ya

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ab
8. y leftof xa
9. ∃x@0:Point. (Colinear(a;y;x@0) ∧ x-x@0-b)
⊢ yab < xab

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  y  leftof  xa  {}\mRightarrow{}  yab  <  xab)


By

---

Latex:
(Auto  THEN  (InstLemma  `use-plane-sep\_strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index