defpred S1[ object , object ] means ex u, v, w, y being VECTOR of V st
( \$1 = [u,v] & \$2 = [w,y] & u,v // w,y );
set VV = [: the carrier of V, the carrier of V:];
consider P being Relation of [: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:] such that
A1: for x, z being object holds
( [x,z] in P iff ( x in [: the carrier of V, the carrier of V:] & z in [: the carrier of V, the carrier of V:] & S1[x,z] ) ) from take P ; :: thesis: for x, z being object holds
( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) )

let x, z be object ; :: thesis: ( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) )

thus ( [x,z] in P implies ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) by A1; :: thesis: ( ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) implies [x,z] in P )

assume ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ; :: thesis: [x,z] in P
hence [x,z] in P by A1; :: thesis: verum