let Y be Subset of X; :: thesis: Y is empty
Y in bool X by Def1;
then Y c= X by ZFMISC_1:def 1;
hence Y is empty ; :: thesis: verum