let S1 be OrderSortedSign; :: thesis: for U1 being OSAlgebra of S1 holds
( U1 is monotone iff MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone )
let U1 be OSAlgebra of S1; :: thesis: ( U1 is monotone iff MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone )
set U2 = MSAlgebra(# the Sorts of U1,the Charact of U1 #);

A1: now

let o1 be OperSymbol of S1; :: thesis: ( Den o1,U1 = Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) & Args o1,U1 = Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) )
thus Den o1,U1 = the Charact of MSAlgebra(# the Sorts of U1,the Charact of U1 #) . o1 by MSUALG_1:def 11
.= Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) by MSUALG_1:def 11 ; :: thesis: Args o1,U1 = Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)
thus Args o1,U1 = ((the Sorts of MSAlgebra(# the Sorts of U1,the Charact of U1 #) # ) * the Arity of S1) . o1 by MSUALG_1:def 9
.= Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) by MSUALG_1:def 9 ; :: thesis: verum

end;

thus ( U1 is monotone implies MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone ) :: thesis: ( MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone implies U1 is monotone )

proof

assume A2: U1 is monotone ; :: thesis: MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone
let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 23 :: thesis: ( not o1 <= o2 or (Den o2,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) | (Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) = Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) )
assume o1 <= o2 ; :: thesis: (Den o2,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) | (Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) = Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)
then A3: (Den o2,U1) | (Args o1,U1) = Den o1,U1 by A2, OSALG_1:def 23;
thus (Den o2,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) | (Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) = (Den o2,U1) | (Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) by A1
.= Den o1,U1 by A1, A3
.= Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) by A1 ; :: thesis: verum

end;

assume A4: MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone ; :: thesis: U1 is monotone
let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 23 :: thesis: ( not o1 <= o2 or (Den o2,U1) | (Args o1,U1) = Den o1,U1 )
assume o1 <= o2 ; :: thesis: (Den o2,U1) | (Args o1,U1) = Den o1,U1
then A5: (Den o2,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) | (Args o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) = Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) by A4, OSALG_1:def 23;
thus (Den o2,U1) | (Args o1,U1) = (Den o2,MSAlgebra(# the Sorts of U1,the Charact of U1 #)) | (Args o1,U1) by A1
.= Den o1,MSAlgebra(# the Sorts of U1,the Charact of U1 #) by A1, A5
.= Den o1,U1 by A1 ; :: thesis: verum