let A be MSAlgebra over S; :: thesis: ( A is non-empty implies not A is empty )
assume the Sorts of A is V2() ; :: according to MSUALG_1:def 3 :: thesis: not A is empty
hence the Sorts of A is V3() ; :: according to CATALG_1:def 2 :: thesis: verum