set VV = [: the carrier of V, the carrier of V:];

defpred S_{1}[ object , object ] means ex u1, u2, v1, v2 being VECTOR of V st

( $1 = [u1,u2] & $2 = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y );

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 uu, vv being object holds

( [uu,vv] in P iff ( uu in [: the carrier of V, the carrier of V:] & vv in [: the carrier of V, the carrier of V:] & S_{1}[uu,vv] ) )
from RELSET_1:sch 1();

take P ; :: thesis: for uu, vv being object holds

( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )

let uu, vv be object ; :: thesis: ( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )

thus ( [uu,vv] in P implies ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) by A1; :: thesis: ( ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) implies [uu,vv] in P )

assume A2: ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ; :: thesis: [uu,vv] in P

then A3: uu in [: the carrier of V, the carrier of V:] by ZFMISC_1:def 2;

vv in [: the carrier of V, the carrier of V:] by A2, ZFMISC_1:def 2;

hence [uu,vv] in P by A1, A2, A3; :: thesis: verum

defpred S

( $1 = [u1,u2] & $2 = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y );

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 uu, vv being object holds

( [uu,vv] in P iff ( uu in [: the carrier of V, the carrier of V:] & vv in [: the carrier of V, the carrier of V:] & S

take P ; :: thesis: for uu, vv being object holds

( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )

let uu, vv be object ; :: thesis: ( [uu,vv] in P iff ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) )

thus ( [uu,vv] in P implies ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ) by A1; :: thesis: ( ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) implies [uu,vv] in P )

assume A2: ex u1, u2, v1, v2 being VECTOR of V st

( uu = [u1,u2] & vv = [v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y ) ; :: thesis: [uu,vv] in P

then A3: uu in [: the carrier of V, the carrier of V:] by ZFMISC_1:def 2;

vv in [: the carrier of V, the carrier of V:] by A2, ZFMISC_1:def 2;

hence [uu,vv] in P by A1, A2, A3; :: thesis: verum