set e = the set ;
reconsider M = I --> { the set } as ManySortedSet of I ;
take M ; :: thesis: M is non-empty
let i be object ; :: according to PBOOLE:def 13 :: thesis: ( i in I implies not M . i is empty )
assume i in I ; :: thesis: not M . i is empty
hence not M . i is empty by FUNCOP_1:7; :: thesis: verum