thus ( not X is empty implies ex Y being set st Y in X ) :: thesis: ( X is empty implies ex b1 being set st b1 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 b1 being set st b1 is empty ) ; :: thesis: verum