theorem Lm1: :: DUALSP05:5

for A being non empty closed_interval Subset of REAL holds the carrier of (ClstoCmp A) = A