Step
*
of Lemma
geo-lt-angle-left2
∀e:EuclideanPlane. ∀a,b,x,y:Point.  (x leftof ab 
⇒ y leftof ab 
⇒ x leftof yb 
⇒ yba < xba)
BY
{ (Auto THEN (InstLemma `use-plane-sep_strict` [⌜e⌝;⌜y⌝;⌜b⌝;⌜x⌝;⌜a⌝]⋅ 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. x leftof yb
⊢ a leftof by
2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ab
8. x leftof yb
9. ∃x@0:Point. (Colinear(y;b;x@0) ∧ x-x@0-a)
⊢ yba < xba
Latex:
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  x  leftof  yb  {}\mRightarrow{}  yba  <  xba)
By
Latex:
(Auto  THEN  (InstLemma  `use-plane-sep\_strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))
Home
Index