consider S being non empty non void ManySortedSign ;
consider A being non empty MSAlgebra of S;
take the Sorts of A ; :: thesis: not the Sorts of A is empty-yielding
thus not the Sorts of A is empty-yielding ; :: thesis: verum