theorem :: LIMFUNC1:1

for seq being Real_Sequence holds
( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )