X \ Y c= X by XBOOLE_1:36;
then X \ Y in bool X by ZFMISC_1:def 1;
hence X \ Y is Subset of X by Def1; :: thesis: verum