:: deftheorem Def1 defines SortsWithConstants MSAFREE2:def 1 :
for S being non empty ManySortedSign holds
( ( not S is void implies SortsWithConstants S = { v where v is SortSymbol of S : v is with_const_op } ) & ( S is void implies SortsWithConstants S = {} ) );