defpred S₁[ 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:] & S₁[x,z] ) ) from RELSET_1:sch 1();
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