theorem Th32: :: RCOMP_3:32

for a, b being Real
for X being Subset of R^1 st a <= b & X = [.a,b.] holds
Fr X = {a,b}