theorem Th2: :: TREAL_1:2
for a, b being Real st a <= b holds
Closed-Interval-TSpace (a,b) is closed