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 3 :: thesis: not A is empty
hence not the Sorts of A is empty-yielding ; :: according to CATALG_1:def 2 :: thesis: verum