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 23 :: 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 22 :: 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 by RELSET_1:34; :: thesis: verum