theorem Th18: :: TOPMETR:18

for a, b being Real st a <= b holds
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by Th10;