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, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) & ( for x, z being object holds
( [x,z] in Q iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) ) implies P = Q )
assume that
A2: for x, z being object holds
( [x,z] in P iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // w,y ) ) and
A3: for x, z being object holds
( [x,z] in Q iff ex u, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // 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, v, w, y being VECTOR of V st
( x = [u,v] & z = [w,y] & u,v // 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