for seq being Real_Sequence st seq is increasing & not seq is bounded_above holds
seq is divergent_to+infty by Th29;