thus ( not X is empty implies ex Y being set st Y in X ) :: thesis: ( X is empty implies ex b₁ being set st b₁ is empty )

proof

assume not X is empty ; :: thesis: ex Y being set st Y in X
then consider Y being object such that
A1: Y in X ;
reconsider Y = Y as set by TARSKI:1;
take Y ; :: thesis: Y in X
thus Y in X by A1; :: thesis: verum

end;

thus ( X is empty implies ex b₁ being set st b₁ is empty ) ; :: thesis: verum