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 )

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

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