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

proof

A3: 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 the Places of N & [y,x] in the Flow of N ) by A1;
hence y in Y by A2; :: 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 the Places of N & [y,x] in the Flow of N ) by A2;
hence y in X by A1; :: thesis: verum

end;

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

end;

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