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