let A, B be set ; :: thesis: bool (A /\ B) = (bool A) /\ (bool B)

now

let x be set ; :: thesis: ( x in bool (A /\ B) iff x in (bool A) /\ (bool B) )
( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
then ( ( x c= A & x c= B ) iff x c= A /\ B ) by XBOOLE_1:1, XBOOLE_1:19;
then ( ( x in bool A & x in bool B ) iff x in bool (A /\ B) ) by Def1;
hence ( x in bool (A /\ B) iff x in (bool A) /\ (bool B) ) by XBOOLE_0:def 4; :: thesis: verum

end;

hence bool (A /\ B) = (bool A) /\ (bool B) by TARSKI:2; :: thesis: verum