let S be OrderSortedSign; :: thesis: for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone
let U1 be non-empty monotone OSAlgebra of S; :: thesis: for R being OSCongruence of U1 holds R is monotone
let R be OSCongruence of U1; :: thesis: R is monotone
let o1, o2 be OperSymbol of S; :: according to OSALG_4:def 28 :: thesis: ( o1 <= o2 implies for x1 being Element of Args o1,U1
for x2 being Element of Args o2,U1 st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2) )
assume A1: o1 <= o2 ; :: thesis: for x1 being Element of Args o1,U1
for x2 being Element of Args o2,U1 st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2)
let x1 be Element of Args o1,U1; :: thesis: for x2 being Element of Args o2,U1 st ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds
[((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2)
let x2 be Element of Args o2,U1; :: thesis: ( ( for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) implies [((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2) )
assume A2: for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ; :: thesis: [((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2)
A3: Den o1,U1 c= Den o2,U1 by A1, OSALG_1:27;
Args o1,U1 c= Args o2,U1 by A1, OSALG_1:26;
then reconsider x3 = x1 as Element of Args o2,U1 by TARSKI:def 3;
A4: [((Den o2,U1) . x3),((Den o2,U1) . x2)] in R . (the_result_sort_of o2) by A2, MSUALG_4:def 6;
x1 in Args o1,U1 ;
then x1 in dom (Den o1,U1) by FUNCT_2:def 1;
hence [((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2) by A3, A4, GRFUNC_1:8; :: thesis: verum