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

defpred S₁[ set ] 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 set 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 set holds
( x in Y iff ( x in union X & S₁[x] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z )
for x being set 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 set ; :: 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 set 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 b₁ being set st b₁ = {} ) ; :: thesis: verum