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

proof

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

end;

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