let P, Q be Relation of [: the carrier of V, the carrier of V:]; ( ( 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 ) ) ) & ( 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_COrtm_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_COrtm_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_COrtm_wrt x,y ) )
; P = Q
for uu, vv being object holds
( [uu,vv] in P iff [uu,vv] in Q )
proof
let uu,
vv be
object ;
( [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 A4;
hence
(
[uu,vv] in P iff
[uu,vv] in Q )
by A5;
verum
end;
hence
P = Q
by RELAT_1:def 2; verum