reconsider s = the carrier of S --> {0} as ManySortedSet of the carrier of S ;
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 object ; :: according to PBOOLE:def 13,MSUALG_1:def 3 :: 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