reconsider s = the carrier of S --> {0} as ManySortedSet of the carrier of S ;
consider o being ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S;
take MSAlgebra(# s,o #) ; :: thesis: ( MSAlgebra(# s,o #) is strict & MSAlgebra(# s,o #) is non-empty )
thus MSAlgebra(# s,o #) is strict ; :: thesis: MSAlgebra(# s,o #) 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 MSAlgebra(# s,o #) . i is empty )
assume i in the carrier of S ; :: thesis: not the Sorts of MSAlgebra(# s,o #) . i is empty
hence not the Sorts of MSAlgebra(# s,o #) . i is empty ; :: thesis: verum