let SM be monotone OrderSortedSign; :: thesis: ( SM is op-discrete implies SM is regular )
assume A1: SM is op-discrete ; :: thesis: SM is regular
let om be OperSymbol of SM; :: according to OSALG_1:def 13 :: thesis: om is regular
thus om is monotone ; :: according to OSALG_1:def 12 :: thesis: for w1 being Element of the carrier of SM * st w1 <= the_arity_of om holds
ex o1 being OperSymbol of SM st o1 has_least_args_for om,w1
let wm1 be Element of the carrier of SM * ; :: thesis: ( wm1 <= the_arity_of om implies ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1 )
assume A2: wm1 <= the_arity_of om ; :: thesis: ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1
om has_least_args_for om,wm1 by A2, A1, Th3;
hence ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1 ; :: thesis: verum