theorem :: RCOMP_3:37

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