let P, Q be Relation of [:the carrier of V,the carrier of V:]; :: thesis: ( ( for uu, vv being set 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 ) ) ) & ( for uu, vv being set holds
( [uu,vv] in Q 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 ) ) ) implies P = Q )
assume that
A3: for uu, vv being set 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 ) ) and
A4: for uu, vv being set holds
( [uu,vv] in Q 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 ) ) ; :: thesis: P = Q
for uu, vv being set holds
( [uu,vv] in P iff [uu,vv] in Q )

proof

let uu, vv be set ; :: thesis: ( [uu,vv] in P iff [uu,vv] in Q )
( [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 ) ) by A3;
hence ( [uu,vv] in P iff [uu,vv] in Q ) by A4; :: thesis: verum

end;

hence P = Q by RELAT_1:def 2; :: thesis: verum