let S be locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
set PTA = ParsedTermsOSA X;
set P = PTCongruence X;
thus PTCongruence X is monotone :: thesis:

let o1, o2 be OperSymbol of S; :: according to OSALG_4:def 26 :: thesis:
assume A1: o1 <= o2 ; :: thesis:
A2: o1 ~= o2 by A1;
A3: the_result_sort_of o1 <= the_result_sort_of o2 by A1;
let x1 be Element of Args (o1,(ParsedTermsOSA X)); :: thesis:
let x2 be Element of Args (o2,(ParsedTermsOSA X)); :: thesis:
assume A4: for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . ((the_arity_of o2) /. y) ; :: thesis:
the_arity_of o1 <= the_arity_of o2 by A1;
then A5: len (the_arity_of o1) = len (the_arity_of o2) ;
then dom (the_arity_of o2) = dom (the_arity_of o1) by FINSEQ_3:29;
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 A4, A2, A3, A5, Th26; :: thesis:

end;