set i = the 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: M is empty-yielding
take the Element of I ; :: according to PBOOLE:def 12 :: thesis: ( the Element of I in I & not M . the Element of I is empty )
thus the Element of I in I ; :: thesis: not M . the Element of I is empty
thus not M . the Element of I is empty by A1; :: thesis: verum