theorem Th10: :: TOPMETR:10

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