let A, B be set ; :: thesis: (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (bool (A \ B)) \/ (bool (B \ A)) or x in bool (A \+\ B) )
assume x in (bool (A \ B)) \/ (bool (B \ A)) ; :: thesis: x in bool (A \+\ B)
then ( x in bool (A \ B) or x in bool (B \ A) ) by XBOOLE_0:def 3;
then A1: ( x c= A \ B or x c= B \ A ) by Def1;
x c= (A \ B) \/ (B \ A)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in (A \ B) \/ (B \ A) )
assume z in x ; :: thesis: z in (A \ B) \/ (B \ A)
then ( z in A \ B or z in B \ A ) by A1, TARSKI:def 3;
hence z in (A \ B) \/ (B \ A) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in bool (A \+\ B) by Def1; :: thesis: verum