let S be OrderSortedSign; :: thesis: ( S is op-discrete implies S is monotone )
set ol = the Overloading of S;
assume S is op-discrete ; :: thesis: S is monotone
then A1: the Overloading of S = id the carrier' of S ;
let o be OperSymbol of S; :: according to OSALG_1:def 8 :: thesis: o is monotone
let o2 be OperSymbol of S; :: according to OSALG_1:def 7 :: thesis: ( o ~= o2 & the_arity_of o <= the_arity_of o2 implies the_result_sort_of o <= the_result_sort_of o2 )
assume o ~= o2 ; :: thesis: ( not the_arity_of o <= the_arity_of o2 or the_result_sort_of o <= the_result_sort_of o2 )
then [o,o2] in the Overloading of S ;
hence ( not the_arity_of o <= the_arity_of o2 or the_result_sort_of o <= the_result_sort_of o2 ) by A1, RELAT_1:def 10; :: thesis: verum