reconsider s = the carrier of S --> {0 } as ManySortedSet of ;
take many-sorted(# s #) ; :: thesis: ( many-sorted(# s #) is strict & many-sorted(# s #) is non-empty )
thus many-sorted(# s #) is strict ; :: thesis: many-sorted(# s #) is non-empty
let i be set ; :: according to PBOOLE:def 16,MSUALG_1:def 8 :: thesis: ( not i in the carrier of S or not the Sorts of many-sorted(# s #) . i is empty )
assume i in the carrier of S ; :: thesis: not the Sorts of many-sorted(# s #) . i is empty
hence not the Sorts of many-sorted(# s #) . i is empty ; :: thesis: verum