:: deftheorem Def7ClstoCmp defines ClstoCmp DUALSP05:def 1 :
for A being non empty closed_interval Subset of REAL
for b₂ being non empty strict compact TopSpace holds
( b₂ = ClstoCmp A iff ex a, b being Real st
( a <= b & [.a,b.] = A & b₂ = Closed-Interval-TSpace (a,b) ) );