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 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 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;
then A3: O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2) by OSALG_1:def 16;
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:18;
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 16;
hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by A3, A4, ZFMISC_1:87; :: thesis: verum