theorem :: TOPMETR3:10

for a, b being Real
for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds
S is convergent