let I be set ; :: thesis: for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B)
let A, B be ManySortedSet of I; :: thesis: bool (A /\ B) = (bool A) /\ (bool B)

now

let i be set ; :: thesis: ( i in I implies (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i )
assume A1: i in I ; :: thesis: (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i
hence (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) by Lm3
.= (bool (A . i)) /\ (bool (B . i)) by ZFMISC_1:71
.= (bool (A . i)) /\ ((bool B) . i) by A1, Def1
.= ((bool A) . i) /\ ((bool B) . i) by A1, Def1
.= ((bool A) /\ (bool B)) . i by A1, PBOOLE:def 5 ;
:: thesis: verum

end;

hence bool (A /\ B) = (bool A) /\ (bool B) by PBOOLE:3; :: thesis: verum