let A, B be set ; :: thesis: (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (bool (A \ B)) \/ (bool (B \ A)) or x in bool (A \+\ B) )
reconsider xx = x as set by TARSKI:1;
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: ( xx c= A \ B or xx c= B \ A ) by Def1;
xx c= (A \ B) \/ (B \ A)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in xx or z in (A \ B) \/ (B \ A) )
assume z in xx ; :: thesis: z in (A \ B) \/ (B \ A)
then ( z in A \ B or z in B \ A ) by A1;
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