let A, B be set ; :: thesis: bool (A \ B) c= {{} } \/ ((bool A) \ (bool B))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool (A \ B) or x in {{} } \/ ((bool A) \ (bool B)) )
assume x in bool (A \ B) ; :: thesis: x in {{} } \/ ((bool A) \ (bool B))
then A1: x c= A \ B by Def1;
( A \ B c= A & A \ B misses B ) by XBOOLE_1:36, XBOOLE_1:79;
then ( x c= A & x misses B ) by A1, XBOOLE_1:1, XBOOLE_1:63;
then ( x c= A & x /\ B = {} ) by XBOOLE_0:def 7;
then ( x = {} or ( x c= A & not x c= B ) ) by XBOOLE_1:28;
then ( x in {{} } or ( x in bool A & not x in bool B ) ) by Def1, TARSKI:def 1;
then ( x in {{} } or x in (bool A) \ (bool B) ) by XBOOLE_0:def 5;
hence x in {{} } \/ ((bool A) \ (bool B)) by XBOOLE_0:def 3; :: thesis: verum