let A be MSAlgebra of S; :: thesis: ( A is non-empty implies not A is empty )
assume the Sorts of A is non-empty ; :: according to MSUALG_1:def 8 :: thesis: not A is empty
then the Sorts of A is V5() ManySortedSet of ;
hence not the Sorts of A is empty-yielding ; :: according to CATALG_1:def 3 :: thesis: verum