let S be locally_directed OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: thesis:
set PTA = ParsedTermsOSA X;
set P = PTCongruence X;
thus PTCongruence X is monotone :: thesis:

proof

let o1, o2 be OperSymbol of S; :: according to OSALG_4:def 28 :: thesis:
assume A1: o1 <= o2 ; :: thesis:
let x1 be Element of Args o1,(ParsedTermsOSA X); :: thesis:
let x2 be Element of Args o2,(ParsedTermsOSA X); :: thesis:
assume A2: for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . ((the_arity_of o2) /. y) ; :: thesis:
A3: ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by A1, OSALG_1:def 22;
then A4: len (the_arity_of o1) = len (the_arity_of o2) by OSALG_1:def 7;
then dom (the_arity_of o2) = dom (the_arity_of o1) by FINSEQ_3:31;
then dom (the_arity_of o2) = dom x1 by MSUALG_3:6;
hence [((Den o1,(ParsedTermsOSA X)) . x1),((Den o2,(ParsedTermsOSA X)) . x2)] in (PTCongruence X) . (the_result_sort_of o2) by A2, A3, A4, Th27; :: thesis:

end;