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 )

( [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

hence
P = Q
by RELAT_1:def 2; :: thesis: verum
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;( [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