theorem Th6: :: TOPMETR3:6

for a, b being Real
for S being sequence of (Closed-Interval-MSpace (a,b)) st a <= b holds
S is sequence of RealSpace