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

proof

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

end;

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

proof

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

end;

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