for SR being monotone regular OrderSortedSign
for o, o3, o4 being OperSymbol of SR
for w1 being Element of the carrier of SR * st o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 holds
o3 = o4