let I be Subset of REAL; :: thesis: ( I is right_open_interval implies I in Borel_Sets )
assume I is right_open_interval ; :: thesis: I in Borel_Sets
then consider a being Real, b being R_eal such that
A1: I = [.a,b.[ by MEASURE5:def 4;
per cases ( b = +infty or b = -infty or b in REAL ) by XXREAL_0:14;
suppose b = +infty ; :: thesis: I in Borel_Sets
then I is Element of Borel_Sets by A1, FINANCE1:3;
hence I in Borel_Sets ; :: thesis: verum
end;
suppose b = -infty ; :: thesis: I in Borel_Sets
then I = {} by A1, XXREAL_0:5, XXREAL_1:27;
hence I in Borel_Sets by MEASURE1:7; :: thesis: verum
end;
suppose b in REAL ; :: thesis: I in Borel_Sets
then I is Element of Borel_Sets by A1, FINANCE1:4;
hence I in Borel_Sets ; :: thesis: verum
end;
end;