let R1, R2 be Relation of the carrier of R; :: thesis: ( ( for x, y being Element of R holds
( [x,y] in R1 iff x in H . {y} ) ) & ( for x, y being Element of R holds
( [x,y] in R2 iff x in H . {y} ) ) implies R1 = R2 )
assume that
A1: for x, y being Element of R holds
( [x,y] in R1 iff x in H . {y} ) and
A2: for x, y being Element of R holds
( [x,y] in R2 iff x in H . {y} ) ; :: thesis: R1 = R2
for x, y being Element of R holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x, y be Element of R; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )
hereby :: thesis: ( [x,y] in R2 implies [x,y] in R1 )
assume [x,y] in R1 ; :: thesis: [x,y] in R2
then x in H . {y} by A1;
hence [x,y] in R2 by A2; :: thesis: verum
end;
assume [x,y] in R2 ; :: thesis: [x,y] in R1
then x in H . {y} by A2;
hence [x,y] in R1 by A1; :: thesis: verum
end;
hence R1 = R2 by RELSET_1:def 2; :: thesis: verum