let S1 be OrderSortedSign; 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; ( 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 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;
( 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
;
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
;
verum end;
thus
( U1 is monotone implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )
( MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone implies U1 is monotone )proof
assume A2:
U1 is
monotone
;
MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone
let o1,
o2 be
OperSymbol of
S1;
OSALG_1:def 21 ( 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
;
(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
;
verum
end;
assume A4:
MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone
; U1 is monotone
let o1, o2 be OperSymbol of S1; OSALG_1:def 21 ( not o1 <= o2 or (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) )
assume
o1 <= o2
; (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
; verum