---

Step * of Lemma r2-left-between

∀a,b,x,y:ℝ^2.  (r2-left(x;a;b) ⇒ rv-T(2;b;y;x) ⇒ b ≠ y ⇒ r2-left(y;a;b))
BY
{ (Unfold `r2-left` 0 THEN Auto THEN Assert ⌜real-vec-be(2;b;y;x)⌝⋅) }

1
.....assertion..... 
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. r0 < |xab|
6. rv-T(2;b;y;x)
7. b ≠ y
⊢ real-vec-be(2;b;y;x)

2
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. r0 < |xab|
6. rv-T(2;b;y;x)
7. b ≠ y
8. real-vec-be(2;b;y;x)
⊢ r0 < |yab|

---

Latex:

---

Latex:
\mforall{}a,b,x,y:\mBbbR{}\^{}2.    (r2-left(x;a;b)  {}\mRightarrow{}  rv-T(2;b;y;x)  {}\mRightarrow{}  b  \mneq{}  y  {}\mRightarrow{}  r2-left(y;a;b))


By

---

Latex:
(Unfold  `r2-left`  0  THEN  Auto  THEN  Assert  \mkleeneopen{}real-vec-be(2;b;y;x)\mkleeneclose{}\mcdot{})

---

Home Index