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