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 :: thesis: for o1 being OperSymbol of S1 holds
( 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 #)) )

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 6
.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def 6 ; :: 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 4
.= Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def 4 ; :: 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 21 :: 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;
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 21 :: 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;
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