let SM be monotone OrderSortedSign; :: thesis:

hereby :: thesis:

assume A1: SM is regular ; :: thesis:
let o be OperSymbol of SM; :: thesis:
let w1 be Element of the carrier of SM * ; :: thesis:
assume A2: w1 <= the_arity_of o ; :: thesis:
o is regular by A1;
then consider o1 being OperSymbol of SM such that
A3: o1 has_least_args_for o,w1 by A2;
take o1 = o1; :: thesis:
o1 has_least_sort_for o,w1

proof

thus A4: ( o ~= o1 & w1 <= the_arity_of o1 ) by A3; :: according to OSALG_1:def 10 :: thesis:
let o2 be OperSymbol of SM; :: thesis:
assume that
A5: o ~= o2 and
A6: w1 <= the_arity_of o2 ; :: thesis:
A7: o1 ~= o2 by A4, A5, Th2;
the_arity_of o1 <= the_arity_of o2 by A3, A5, A6;
hence the_result_sort_of o1 <= the_result_sort_of o2 by A7, Def7; :: thesis:

end;

hence o1 has_least_rank_for o,w1 by A3; :: thesis:

end;

assume A8: for o being OperSymbol of SM
for w1 being Element of the carrier of SM * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1 ; :: thesis:
let o be OperSymbol of SM; :: according to OSALG_1:def 13 :: thesis:
thus o is monotone ; :: according to OSALG_1:def 12 :: thesis:
let w1 be Element of the carrier of SM * ; :: thesis:
assume w1 <= the_arity_of o ; :: thesis:
then consider o1 being OperSymbol of SM such that
A9: o1 has_least_rank_for o,w1 by A8;
take o1 ; :: thesis:
thus o1 has_least_args_for o,w1 by A9; :: thesis: