let I be set ; :: thesis: for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds
M is non-empty
let M be ManySortedSet of I; :: thesis: ( ex A being ManySortedSet of I st A in M implies M is non-empty )
given A being ManySortedSet of I such that A1: A in M ; :: thesis: M is non-empty
let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not M . i is empty )
assume i in I ; :: thesis: not M . i is empty
hence not M . i is empty by A1, PBOOLE:def 4; :: thesis: verum