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 14 :: thesis: om is regular
thus om is monotone ; :: according to OSALG_1:def 13 :: 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

proof

thus ( om ~= om & wm1 <= the_arity_of om ) by A2; :: according to OSALG_1:def 10 :: thesis: for o2 being OperSymbol of SM st om ~= o2 & wm1 <= the_arity_of o2 holds
the_arity_of om <= the_arity_of o2
let om2 be OperSymbol of SM; :: thesis: ( om ~= om2 & wm1 <= the_arity_of om2 implies the_arity_of om <= the_arity_of om2 )
assume that
A3: om ~= om2 and
wm1 <= the_arity_of om2 ; :: thesis: the_arity_of om <= the_arity_of om2
thus the_arity_of om <= the_arity_of om2 by A1, A3, Th3; :: thesis: verum

end;

hence ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1 ; :: thesis: verum