let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st y = (v + w) - u holds
( u,v // w,y & u,w // v,y )
let u, v, w, y be VECTOR of V; :: thesis: ( y = (v + w) - u implies ( u,v // w,y & u,w // v,y ) )
set y = (v + w) - u;
((v + w) - u) + u = v + w by RLSUB_2:61;
then ( ((v + w) - u) - v = w - u & ((v + w) - u) - w = v - u ) by Th2;
hence ( y = (v + w) - u implies ( u,v // w,y & u,w // v,y ) ) by Th15; :: thesis: verum