let P, Q be Relation of [: the carrier of V, the carrier of V:]; ( ( for x, z being object holds
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being object holds
( [x,z] in Q iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) implies P = Q )
assume that
A2:
for x, z being object holds
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
and
A3:
for x, z being object holds
( [x,z] in Q iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
; P = Q
for x, z being object holds
( [x,z] in P iff [x,z] in Q )
proof
let x,
z be
object ;
( [x,z] in P iff [x,z] in Q )
(
[x,z] in P iff ex
u,
u1,
v,
v1 being
VECTOR of
V st
(
x = [u,u1] &
z = [v,v1] &
u,
u1,
v,
v1 are_Ort_wrt w,
y ) )
by A2;
hence
(
[x,z] in P iff
[x,z] in Q )
by A3;
verum
end;
hence
P = Q
by RELAT_1:def 2; verum