let I be Subset of REAL; :: thesis: ( I is open_interval implies I in Borel_Sets )
assume I is open_interval ; :: thesis: I in Borel_Sets
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 ( a = +infty or a = -infty or a in REAL ) by XXREAL_0:14;

suppose a = +infty ; :: thesis: I in Borel_Sets

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

end;

suppose A3: a = -infty ; :: thesis: I in Borel_Sets

per cases ( b = +infty or b = -infty or b in REAL ) by XXREAL_0:14;

suppose b = +infty ; :: thesis: I in Borel_Sets

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

end;

suppose b = -infty ; :: thesis: I in Borel_Sets

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

end;

suppose A4: b in REAL ; :: thesis: I in Borel_Sets

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: verum

end;

end;

end;

suppose A8: a in REAL ; :: thesis: I in Borel_Sets

then reconsider a1 = a as Real ;

per cases ( b = +infty or b = -infty or b in REAL ) by XXREAL_0:14;

suppose A6: b = +infty ; :: thesis: I in Borel_Sets

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: verum

end;

suppose b = -infty ; :: thesis: I in Borel_Sets

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

end;

suppose b in REAL ; :: thesis: I in Borel_Sets

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

per cases ( a < b or a >= b ) ;

suppose a < b ; :: thesis: I in Borel_Sets

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

end;

suppose a >= b ; :: thesis: I in Borel_Sets

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

end;

end;

end;

end;

end;

end;