let Z1, Z2 be set ; :: thesis: ( ( X <> {} & ( for x being set holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being set holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) )

now

assume that
A5: ( X <> {} & ( for x being set holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) ) and
A6: for x being set holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ; :: thesis: Z1 = Z2

now

let x be set ; :: thesis: ( x in Z1 iff x in Z2 )
( x in Z1 iff for Y being set st Y in X holds
x in Y ) by A5;
hence ( x in Z1 iff x in Z2 ) by A6; :: thesis: verum

end;

hence Z1 = Z2 by TARSKI:2; :: thesis: verum

end;

hence ( ( X <> {} & ( for x being set holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being set holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) ) ; :: thesis: verum