Step * of Lemma geo-lt-angle-left2

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

1
.....antecedent..... 
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. leftof ab
7. leftof ab
8. leftof yb
⊢ leftof by

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. leftof ab
7. leftof ab
8. 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