let Z1, Z2 be set ; :: thesis: ( ( X <> {} & ( for x being object holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being object 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 :: thesis: ( X <> {} & ( for x being object holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being object holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ) implies Z1 = Z2 )

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

now :: thesis: for x being object holds
( x in Z1 iff x in Z2 )

let x be object ; :: 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 A4;
hence ( x in Z1 iff x in Z2 ) by A5; :: thesis: verum

end;

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

end;

hence ( ( X <> {} & ( for x being object holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being object 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