theorem :: RCOMP_3:33

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