thus ( X <> {} implies ex Z1 being set st
for x being set holds
( x in Z1 iff for Z being set st Z in X holds
x in Z ) ) :: thesis: ( not X <> {} implies ex b₁ being set st b₁ = {} )

proof

assume A1: X <> {} ; :: thesis: ex Z1 being set st
for x being set holds
( x in Z1 iff for Z being set st Z in X holds
x in Z )
defpred S₁[ set ] means for Z being set st Z in X holds
$1 in Z;
consider Y being set such that
A2: for x being set holds
( x in Y iff ( x in union X & S₁[x] ) ) from XBOOLE_0:sch 1();
A3: for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z )

proof

for x being set st ( for Z being set st Z in X holds
x in Z ) holds
x in Y

proof

let x be set ; :: thesis: ( ( for Z being set st Z in X holds
x in Z ) implies x in Y )
assume A4: for Z being set st Z in X holds
x in Z ; :: thesis: x in Y
consider y being Element of X;
x in y by A1, A4;
then x in union X by A1, TARSKI:def 4;
hence x in Y by A2, A4; :: thesis: verum

end;

hence for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z ) by A2; :: thesis: verum

end;

take Y ; :: thesis: for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z )
thus for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z ) by A3; :: thesis: verum

end;

thus ( not X <> {} implies ex b₁ being set st b₁ = {} ) ; :: thesis: verum