set VV = [: the carrier of V, the carrier of V:];
defpred S1[ object , object ] means ex u1, u2, v1, v2 being VECTOR of V st
( \$1 = [u1,u2] & \$2 = [v1,v2] & u1,u2,v1,v2 are_COrtm_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:] & S1[uu,vv] ) ) from 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_COrtm_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_COrtm_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_COrtm_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_COrtm_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_COrtm_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 ;
hence [uu,vv] in P by A1, A2, A3; :: thesis: verum