theorem Th27: :: OSALG_1:27

for S being 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) )