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