set VV = [: the carrier of V, the carrier of V:];
defpred S₁[ 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:] & S₁[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_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 A2, ZFMISC_1:def 2;
hence [uu,vv] in P by A1, A2, A3; :: thesis: verum