:: deftheorem Def26 defines monotone OSALG_4:def 26 :
for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being MSEquivalence-like OrderSortedRelation of U1 holds
( R is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
for x1 being Element of Args (o1,U1)
for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) );