theorem Th19: :: TOPMETR:19

for a, b being Real st a <= b holds
for P being Subset of R^1 st P = [.a,b.] holds
Closed-Interval-TSpace (a,b) = R^1 | P