let S be OrderSortedSign; :: thesis: 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; :: thesis: ( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) )

hereby :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ( o1 <= o2 implies Den (o1,A) c= Den (o2,A) )
assume o1 <= o2 ; :: thesis: 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; :: thesis: verum

end;

assume A2: for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) ; :: thesis: A is monotone
let o1 be OperSymbol of S; :: according to OSALG_1:def 21 :: thesis: 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; :: thesis: ( o1 <= o2 implies (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) )
assume A3: o1 <= o2 ; :: thesis: (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) ;
:: thesis: verum