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

now :: thesis: for i being object st i in I holds
(bool {x}) . i = {(EmptyMS I),{x}} . i

let i be object ; :: thesis: ( i in I implies (bool {x}) . i = {(EmptyMS I),{x}} . i )
assume A1: i in I ; :: thesis: (bool {x}) . i = {(EmptyMS 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
.= {((EmptyMS I) . i),{(x . i)}} by PBOOLE:5
.= {((EmptyMS I) . i),({x} . i)} by A1, Def1
.= {(EmptyMS I),{x}} . i by A1, Def2 ;
:: thesis: verum

end;

hence bool {x} = {(EmptyMS I),{x}} ; :: thesis: verum