let A, B be set ; :: thesis: bool (A \ B) c= {{}} \/ ((bool A) \ (bool B))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool (A \ B) or x in {{}} \/ ((bool A) \ (bool B)) )
reconsider xx = x as set by TARSKI:1;
assume x in bool (A \ B) ; :: thesis: x in {{}} \/ ((bool A) \ (bool B))
then A1: xx c= A \ B by Def1;
then xx misses B by XBOOLE_1:63, XBOOLE_1:79;
then ( A \ B c= A & xx /\ B = {} ) by XBOOLE_1:36;
then ( x = {} or ( xx c= A & not xx c= B ) ) by A1, 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