theorem :: RCOMP_3:36

for a, b being Real
for X being Subset of R^1 st X = [.a,b.] holds
Int X = ].a,b.[