let S be OrderSortedSign; :: thesis: for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 st R = [|the Sorts of U1,the Sorts of U1|] holds
R is monotone
let U1 be non-empty OSAlgebra of S; :: thesis: for R being OSCongruence of U1 st R = [|the Sorts of U1,the Sorts of U1|] holds
R is monotone
let R be OSCongruence of U1; :: thesis: ( R = [|the Sorts of U1,the Sorts of U1|] implies R is monotone )
assume A1: R = [|the Sorts of U1,the Sorts of U1|] ; :: thesis: R is monotone
reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
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 A2: 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)
set s2 = the_result_sort_of o2;
set s1 = the_result_sort_of o1;
the_result_sort_of o1 <= the_result_sort_of o2 by A2, OSALG_1:def 22;
then A3: O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2) by OSALG_1:def 18;
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 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)
A4: ( (Den o1,U1) . x1 in the Sorts of U1 . (the_result_sort_of o1) & (Den o2,U1) . x2 in the Sorts of U1 . (the_result_sort_of o2) ) by MSUALG_9:19;
R . (the_result_sort_of o2) = [:(the Sorts of U1 . (the_result_sort_of o2)),(the Sorts of U1 . (the_result_sort_of o2)):] by A1, PBOOLE:def 21;
hence [((Den o1,U1) . x1),((Den o2,U1) . x2)] in R . (the_result_sort_of o2) by A3, A4, ZFMISC_1:106; :: thesis: verum