theorem Th23: :: COUSIN:26

for a, b being Real_Sequence st ( for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) holds
IntervalSequence (a,b) is non-ascending