theorem Th17: :: COUSIN:20

for a, b being Real_Sequence holds IntervalSequence (a,b) is SetSequence of (Euclid 1)