:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :
for S being non void Signature
for s being SortSymbol of S st ex o being OperSymbol of S st the_result_sort_of o = s holds
for b₃ being OperSymbol of S holds
( b₃ is OperSymbol of s iff the_result_sort_of b₃ = s );