let S be OrderSortedSign; for A being non-empty OSAlgebra of S holds
( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) )
let A be non-empty OSAlgebra of S; ( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) )
hereby ( ( for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) ) implies A is monotone )
assume A1:
A is
monotone
;
for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A)let o1,
o2 be
OperSymbol of
S;
( o1 <= o2 implies Den (o1,A) c= Den (o2,A) )assume
o1 <= o2
;
Den (o1,A) c= Den (o2,A)then
(Den (o2,A)) | (Args (o1,A)) = Den (
o1,
A)
by A1;
hence
Den (
o1,
A)
c= Den (
o2,
A)
by RELAT_1:59;
verum
end;
assume A2:
for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A)
; A is monotone
let o1 be OperSymbol of S; OSALG_1:def 21 for o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
let o2 be OperSymbol of S; ( o1 <= o2 implies (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) )
assume A3:
o1 <= o2
; (Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
dom (Den (o1,A)) = Args (o1,A)
by FUNCT_2:def 1;
hence (Den (o2,A)) | (Args (o1,A)) =
(Den (o1,A)) | (Args (o1,A))
by A2, A3, GRFUNC_1:27
.=
Den (o1,A)
;
verum