let V be RealLinearSpace; for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds
ex r being Real st
( v - u = r * (w - v) & 0 < r )
let u, v, w be VECTOR of V; ( u <> v & w <> v & u,v // v,w implies ex r being Real st
( v - u = r * (w - v) & 0 < r ) )
assume
( u <> v & w <> v & u,v // v,w )
; ex r being Real st
( v - u = r * (w - v) & 0 < r )
then consider a, b being Real such that
A1:
a * (v - u) = b * (w - v)
and
A2:
0 < a
and
A3:
0 < b
by ANALOAF:7;
take r = (a ") * b; ( v - u = r * (w - v) & 0 < r )
0 < a "
by A2, XREAL_1:122;
then A4:
0 * b < r
by A3, XREAL_1:68;
v - u =
1 * (v - u)
by RLVECT_1:def 8
.=
((a ") * a) * (v - u)
by A2, XCMPLX_0:def 7
.=
(a ") * (b * (w - v))
by A1, RLVECT_1:def 7
.=
r * (w - v)
by RLVECT_1:def 7
;
hence
( v - u = r * (w - v) & 0 < r )
by A4; verum