A1: A in bool E by Def2;
A2: A \ X c= A by XBOOLE_1:36;
A c= E by A1, ZFMISC_1:def 1;
then A \ X c= E by A2, XBOOLE_1:1;
then A \ X in bool E by ZFMISC_1:def 1;
hence A \ X is Subset of E by Def2; :: thesis: verum