consider i being Element of I;
let M be ManySortedSet of I; :: thesis: ( M is non-empty implies not M is empty-yielding )
assume A1: M is non-empty ; :: thesis: not M is empty-yielding
take i ; :: according to PBOOLE:def 15 :: thesis: ( i in I & not M . i is empty )
thus i in I ; :: thesis: not M . i is empty
thus not M . i is empty by A1, Def16; :: thesis: verum