:: deftheorem Def13 defines regular OSALG_1:def 13 :
for SM being monotone OrderSortedSign holds
( SM is regular iff for om being OperSymbol of SM holds om is regular );