let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V st u,v // v,w holds
u,v // u,w
let u, v, w be VECTOR of V; :: thesis: ( u,v // v,w implies u,v // u,w )
assume A1:
u,v // v,w
; :: thesis: u,v // u,w
now assume
(
u <> v &
v <> w )
;
:: thesis: u,v // u,wthen consider a,
b being
Real such that A2:
(
a * (v - u) = b * (w - v) &
0 < a &
0 < b )
by A1, Th16;
A3:
b * (w - u) =
b * ((w - v) + (v - u))
by Th4
.=
(a * (v - u)) + (b * (v - u))
by A2, RLVECT_1:def 9
.=
(a + b) * (v - u)
by RLVECT_1:def 9
;
0 < a + b
by A2, XREAL_1:36;
hence
u,
v // u,
w
by A2, A3, Def1;
:: thesis: verum end;
hence
u,v // u,w
by Def1, Th17; :: thesis: verum