let I be set ; :: thesis: for A being ManySortedSet of I holds {A} c= bool A
let A be ManySortedSet of I; :: thesis: {A} c= bool A
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or {A} . i c= (bool A) . i )
assume A1: i in I ; :: thesis: {A} . i c= (bool A) . i
{(A . i)} c= bool (A . i) by ZFMISC_1:68;
then {A} . i c= bool (A . i) by A1, Def1;
hence {A} . i c= (bool A) . i by A1, MBOOLEAN:def 1; :: thesis: verum