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 A2: o1 <= o2 ; :: thesis: Den o1,A c= Den o2,A
(Den o2,A) | (Args o1,A) = Den o1,A by A1, A2, Def23;
hence Den o1,A c= Den o2,A by RELAT_1:88; :: thesis: verum

end;

assume A3: 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 23 :: 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 A4: o1 <= o2 ; :: thesis: (Den o2,A) | (Args o1,A) = Den o1,A
A5: ( dom (Den o1,A) = Args o1,A & dom (Den o2,A) = Args o2,A ) by FUNCT_2:def 1;
hence (Den o2,A) | (Args o1,A) = (Den o1,A) | (Args o1,A) by A3, A4, GRFUNC_1:95
.= Den o1,A by A5, RELAT_1:98 ;
:: thesis: verum