for I being Subset of REAL st I is Interval holds
I in Borel_Sets