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