defpred S_{1}[ 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_{1}[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

( $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

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