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 10;
hence Y is empty-membered by SETFAM_1:def 10; :: thesis: verum