let I be Subset of REAL; :: thesis:
assume I is open_interval ; :: thesis:
then consider a, b being R_eal such that
A1: I = ].a,b.[ by MEASURE5:def 2;
A2: Family_of_halflines c= Borel_Sets by PROB_1:def 9, PROB_1:def 12;

per cases by XXREAL_0:14;

suppose a = +infty ; :: thesis:

then I = {} by A1, XXREAL_0:3, XXREAL_1:28;
hence I in Borel_Sets by MEASURE1:7; :: thesis:

end;

suppose A3: a = -infty ; :: thesis:

per cases by XXREAL_0:14;

suppose b = +infty ; :: thesis:

hence I in Borel_Sets by A1, A3, XXREAL_1:224, FINANCE2:11; :: thesis:

end;

suppose b = -infty ; :: thesis:

then I = {} by A1, A3, XXREAL_1:20;
hence I in Borel_Sets by MEASURE1:7; :: thesis:

end;

suppose A4: b in REAL ; :: thesis:

I = halfline b by A1, A3, PROB_1:def 10;
then I in Family_of_halflines by A4, PROB_1:def 11;
hence I in Borel_Sets by A2; :: thesis:

end;

end;

end;

suppose A8: a in REAL ; :: thesis:

then reconsider a1 = a as Real ;

per cases by XXREAL_0:14;

suppose A6: b = +infty ; :: thesis:

then [.a1,b.[ is Element of Borel_Sets by FINANCE1:3;
then A7: ( {a} in Borel_Sets & [.a,b.[ in Borel_Sets ) by FINANCE2:5;
I = [.a,b.[ \ {a} by A1, A6, A8, XXREAL_0:9, XXREAL_1:136;
hence I in Borel_Sets by A7, MEASURE1:6; :: thesis:

end;

suppose b = -infty ; :: thesis:

then I = {} by A1, XXREAL_1:210;
hence I in Borel_Sets by MEASURE1:7; :: thesis:

end;

suppose b in REAL ; :: thesis:

then A9: ( ].a,b.] is Element of Borel_Sets & {b} is Element of Borel_Sets ) by A8, FINANCE2:5, FINANCE2:6;

per cases ;

suppose a < b ; :: thesis:

then I = ].a,b.] \ {b} by A1, XXREAL_1:137;
hence I in Borel_Sets by A9, MEASURE1:6; :: thesis:

end;

suppose a >= b ; :: thesis:

then I = {} by A1, XXREAL_1:28;
hence I in Borel_Sets by MEASURE1:7; :: thesis:

end;

end;

end;

end;

end;

end;