let I be Subset of REAL; :: thesis: ( I is Interval implies I in Borel_Sets )
assume I is Interval ; :: thesis: I in Borel_Sets
then ( I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval ) by MEASURE5:1;
hence I in Borel_Sets by Lm01, Lm02, Lm03, Lm04; :: thesis: verum