for seq being Real_Sequence st seq is non-decreasing holds
for n being Nat holds seq . 0 <= seq . n by Th6;