let X, Y be set ; :: thesis: ( ( for y being set holds
( y in X iff ( y in Elements N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in Y iff ( y in Elements N & [x,y] in the Flow of N ) ) ) implies X = Y )
assume that
A4: for y being set holds
( y in X iff ( y in Elements N & [x,y] in the Flow of N ) ) and
A5: for y being set holds
( y in Y iff ( y in Elements N & [x,y] in the Flow of N ) ) ; :: thesis: X = Y
for y being set holds
( y in X iff y in Y )

proof

A6: for y being set st y in X holds
y in Y

proof

let y be set ; :: thesis: ( y in X implies y in Y )
assume y in X ; :: thesis: y in Y
then ( y in Elements N & [x,y] in the Flow of N ) by A4;
hence y in Y by A5; :: thesis: verum

end;

for y being set st y in Y holds
y in X

proof

let y be set ; :: thesis: ( y in Y implies y in X )
assume y in Y ; :: thesis: y in X
then ( y in Elements N & [x,y] in the Flow of N ) by A5;
hence y in X by A4; :: thesis: verum

end;

hence for y being set holds
( y in X iff y in Y ) by A6; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum