thus ( X <> {} implies ex Z1 being set st
for x being object holds
( x in Z1 iff for Z being set st Z in X holds
x in Z ) ) :: thesis: ( not X <> {} implies ex b1 being set st b1 = {} )
proof
defpred S1[ object ] means for Z being set st Z in X holds
$1 in Z;
assume A1: X <> {} ; :: thesis: ex Z1 being set st
for x being object holds
( x in Z1 iff for Z being set st Z in X holds
x in Z )
consider Y being set such that
A2: for x being object holds
( x in Y iff ( x in union X & S1[x] ) ) from XBOOLE_0:sch 1();
 take Y ; :: thesis: for x being object holds
( x in Y iff for Z being set st Z in X holds
x in Z )
for x being object st ( for Z being set st Z in X holds
x in Z ) holds
x in Y
proof
set y = the Element of X;
let x be object ; :: thesis: ( ( for Z being set st Z in X holds
x in Z ) implies x in Y )
assume A3: for Z being set st Z in X holds
x in Z ; :: thesis: x in Y
x in the Element of X by A1, A3;
then x in union X by A1, TARSKI:def 4;
hence x in Y by A2, A3; :: thesis: verum
end;
hence for x being object holds
( x in Y iff for Z being set st Z in X holds
x in Z ) by A2; :: thesis: verum
end;
thus ( not X <> {} implies ex b1 being set st b1 = {} ) ; :: thesis: verum