let X, Y be set ; :: thesis: ( ( for y being object holds
( y in X iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being object holds
( y in Y iff ( y in Elements N & [y,x] in Flow N ) ) ) implies X = Y )
assume that
A1: for y being object holds
( y in X iff ( y in Elements N & [y,x] in Flow N ) ) and
A2: for y being object holds
( y in Y iff ( y in Elements N & [y,x] in Flow N ) ) ; :: thesis: X = Y
A3: 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 & [y,x] in Flow N ) by A2;
hence y in X by A1; :: 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 & [y,x] in Flow N ) by A1;
hence y in Y by A2; :: thesis: verum

end;

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