let I be set ; :: thesis: for x being ManySortedSet of I holds bool {x} = {([[0]] I),{x}}
let x be ManySortedSet of I; :: thesis: bool {x} = {([[0]] I),{x}}

now

let i be set ; :: thesis: ( i in I implies (bool {x}) . i = {([[0]] I),{x}} . i )
assume A1: i in I ; :: thesis: (bool {x}) . i = {([[0]] I),{x}} . i
hence (bool {x}) . i = bool ({x} . i) by MBOOLEAN:def 1
.= bool {(x . i)} by A1, Def1
.= {{},{(x . i)}} by ZFMISC_1:24
.= {(([[0]] I) . i),{(x . i)}} by PBOOLE:5
.= {(([[0]] I) . i),({x} . i)} by A1, Def1
.= {([[0]] I),{x}} . i by A1, Def2 ;
:: thesis: verum

end;

hence bool {x} = {([[0]] I),{x}} by PBOOLE:3; :: thesis: verum