for seq being Real_Sequence st seq is decreasing & not seq is bounded_below holds
seq is divergent_to-infty by Th30;