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 )

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

hence
R1 = R2
by RELSET_1:def 2; :: thesis: verum
let x, y be Element of R; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )

then x in H . {y} by A2;

hence [x,y] in R1 by A1; :: thesis: verum

end;hereby :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

assume
[x,y] in R2
; :: thesis: [x,y] in R1assume
[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;then x in H . {y} by A1;

hence [x,y] in R2 by A2; :: thesis: verum

then x in H . {y} by A2;

hence [x,y] in R1 by A1; :: thesis: verum