let Y be Subset of X; :: thesis: Y is empty-membered
for x being non empty set holds not x in Y by SETFAM_1:def 11;
hence Y is empty-membered by SETFAM_1:def 11; :: thesis: verum