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 26 :: 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)
Args (o1,U1) c= Args (o2,U1) by A1, OSALG_1:26;
then reconsider x3 = x1 as Element of Args (o2,U1) ;
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 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)
then A2: [((Den (o2,U1)) . x3),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by MSUALG_4:def 4;
x1 in Args (o1,U1) ;
then A3: x1 in dom (Den (o1,U1)) by FUNCT_2:def 1;
Den (o1,U1) c= Den (o2,U1) by A1, OSALG_1:27;
hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by A2, A3, GRFUNC_1:2; :: thesis: verum