theorem Th22: :: COUSIN:25

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-empty pointwise_bounded closed SetSequence of (Euclid 1)