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 RELSET_1:sch 1();
take
P
; 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 ; ( [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; ( 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 )
; [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; verum