:: deftheorem Def3 defines discernable OSALG_1:def 3 :
for S being non empty non void OverloadedMSSign holds
( S is discernable iff for x, y being OperSymbol of S st x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y holds
x = y );