let S be OrderSortedSign; :: thesis: 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; :: thesis: ( ( S is discrete or S is op-discrete ) implies A is monotone )
assume A1: ( S is discrete or S is op-discrete ) ; :: thesis: A is monotone
let o1 be OperSymbol of S; :: according to OSALG_1:def 21 :: thesis: 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; :: thesis: ( 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 ) ; :: according to OSALG_1:def 20 :: thesis: (Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
o1 = o2

proof

per cases ( S is discrete or S is op-discrete ) by A1;

suppose S is discrete ; :: thesis: o1 = o2

hence o1 = o2 by A2, A3, Th8; :: thesis: verum

end;

suppose S is op-discrete ; :: thesis: o1 = o2

hence o1 = o2 by A2, Th3; :: thesis: verum

end;

end;

end;

hence (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) ; :: thesis: verum