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 :: thesis: ( u <> v & v <> w implies u,v // u,w )
assume ( u <> v & v <> w ) ; :: thesis: u,v // u,w
then consider a, b being Real such that
A2: a * (v - u) = b * (w - v) and
A3: 0 < a and
A4: 0 < b by A1;
A5: 0 < a + b by A3, A4;
b * (w - u) = b * ((w - v) + (v - u)) by Th1
.= (a * (v - u)) + (b * (v - u)) by A2, RLVECT_1:def 5
.= (a + b) * (v - u) by RLVECT_1:def 6 ;
hence u,v // u,w by A4, A5; :: thesis: verum
end;
hence u,v // u,w by Th8; :: thesis: verum