let SM be monotone OrderSortedSign; :: thesis: ( SM is regular iff 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 )

hereby :: thesis: ( ( 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 ) implies SM is regular )

assume A1: SM is regular ; :: thesis: 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
let o be OperSymbol of SM; :: thesis: 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
let w1 be Element of the carrier of SM * ; :: thesis: ( w1 <= the_arity_of o implies ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1 )
A2: o is regular by A1, Def14;
assume w1 <= the_arity_of o ; :: thesis: ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1
then consider o1 being OperSymbol of SM such that
A3: o1 has_least_args_for o,w1 by A2, Def13;
take o1 = o1; :: thesis: o1 has_least_rank_for o,w1
o1 has_least_sort_for o,w1

proof

thus A4: ( o ~= o1 & w1 <= the_arity_of o1 ) by A3, Def10; :: according to OSALG_1:def 11 :: thesis: for o2 being OperSymbol of SM st o ~= o2 & w1 <= the_arity_of o2 holds
the_result_sort_of o1 <= the_result_sort_of o2
let o2 be OperSymbol of SM; :: thesis: ( o ~= o2 & w1 <= the_arity_of o2 implies the_result_sort_of o1 <= the_result_sort_of o2 )
assume A5: ( o ~= o2 & w1 <= the_arity_of o2 ) ; :: thesis: the_result_sort_of o1 <= the_result_sort_of o2
then A6: the_arity_of o1 <= the_arity_of o2 by A3, Def10;
o1 ~= o2 by A4, A5, Th2;
hence the_result_sort_of o1 <= the_result_sort_of o2 by A6, Def8; :: thesis: verum

end;

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

end;

assume A7: 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: SM is regular
let o be OperSymbol of SM; :: according to OSALG_1:def 14 :: thesis: o is regular
thus o is monotone ; :: according to OSALG_1:def 13 :: thesis: 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_args_for o,w1
let w1 be Element of the carrier of SM * ; :: thesis: ( w1 <= the_arity_of o implies ex o1 being OperSymbol of SM st o1 has_least_args_for o,w1 )
assume A8: w1 <= the_arity_of o ; :: thesis: ex o1 being OperSymbol of SM st o1 has_least_args_for o,w1
consider o1 being OperSymbol of SM such that
A9: o1 has_least_rank_for o,w1 by A7, A8;
take o1 ; :: thesis: o1 has_least_args_for o,w1
thus o1 has_least_args_for o,w1 by A9, Def12; :: thesis: verum