let S be OrderSortedSign; for A being OSAlgebra of S st ( S is discrete or S is op-discrete ) holds
A is monotone
let A be OSAlgebra of S; ( ( S is discrete or S is op-discrete ) implies A is monotone )
assume A1:
( S is discrete or S is op-discrete )
; A is monotone
let o1 be OperSymbol of S; OSALG_1:def 21 for o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
let o2 be OperSymbol of S; ( o1 <= o2 implies (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) )
assume that
A2:
o1 ~= o2
and
A3:
( the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 )
; OSALG_1:def 20 (Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
o1 = o2
hence
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
; verum