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 b_{1} being set st b_{1} = {} )_{1} being set st b_{1} = {} )
; :: thesis: verum

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 b

proof

thus
( not X <> {} implies ex b
defpred S_{1}[ 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 & S_{1}[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

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

x in Z ) by A2; :: thesis: verum

end;$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 & S

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

hence
for x being object holds
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;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

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

x in Z ) by A2; :: thesis: verum