let S be non empty non void OverloadedMSSign ; :: thesis: ( S is op-discrete implies S is discernable )
assume A1: S is op-discrete ; :: thesis: S is discernable
let x, y be OperSymbol of S; :: according to OSALG_1:def 3 :: thesis: ( x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y implies x = y )
thus ( x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y implies x = y ) by A1, Th3; :: thesis: verum