let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st u,v // w,y & u <> v & w <> y holds
ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b )
let u, v, w, y be VECTOR of V; :: thesis: ( u,v // w,y & u <> v & w <> y implies ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b ) )
assume that
A1: u,v // w,y and
A2: ( u <> v & w <> y ) ; :: thesis: ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b )
( u = v or w = y or ex a, b being Real st
( 0 < a & 0 < b & a * (v - u) = b * (y - w) ) ) by A1, Def1;
hence ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b ) by A2; :: thesis: verum