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