let A, B be set ; :: thesis: bool (A /\ B) = (bool A) /\ (bool B)
now :: thesis: for x being object holds
( x in bool (A /\ B) iff x in (bool A) /\ (bool B) )
let x be object ; :: thesis: ( x in bool (A /\ B) iff x in (bool A) /\ (bool B) )
reconsider xx = x as set by TARSKI:1;
( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
then ( ( xx c= A & xx c= B ) iff xx c= A /\ B ) by 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