for seq being Real_Sequence st seq is non-increasing & not seq is bounded_below holds
seq is divergent_to-infty