let P, Q be Relation of [: the carrier of V, the carrier of V:]; :: thesis: ( ( 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_DTr_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_DTr_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_DTr_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_DTr_wrt w,y ) ) ; :: thesis: P = Q
for x, z being object holds
( [x,z] in P iff [x,z] in Q )

proof

let x, z be object ; :: thesis: ( [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_DTr_wrt w,y ) ) by A2;
hence ( [x,z] in P iff [x,z] in Q ) by A3; :: thesis: verum

end;

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