A in bool E by Def1;
then ( A \ X c= A & A c= E ) by XBOOLE_1:36, ZFMISC_1:def 1;
then A \ X c= E ;
then A \ X in bool E by ZFMISC_1:def 1;
hence A \ X is Subset of E by Def1; :: thesis: verum