thus ( X <> {} implies ex Y being set st
for x being Function st x in X holds
Y = dom x ) :: thesis: ( not X <> {} implies ex b₁ being set st b₁ = {} )

proof

assume X <> {} ; :: thesis: ex Y being set st
for x being Function st x in X holds
Y = dom x
then consider x being set such that
A1: x in X by XBOOLE_0:def 1;
reconsider x = x as Function by A1;
take dom x ; :: thesis: for x being Function st x in X holds
dom x = dom x
thus for x being Function st x in X holds
dom x = dom x by A1, Def10; :: thesis: verum

end;

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