:: deftheorem SR defines sufficiently_rich MSAFREE5:def 4 :
for S being non empty non void ManySortedSign holds
( S is sufficiently_rich iff for s being SortSymbol of S ex o being OperSymbol of S st s in rng (the_arity_of o) );