let I be Subset of REAL; :: thesis: ( I is left_open_interval implies I in Borel_Sets )
assume I is left_open_interval ; :: thesis: I in Borel_Sets
then consider a being R_eal, b being Real such that
A1: I = ].a,b.] by MEASURE5:def 5;
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:26;
hence I in Borel_Sets by MEASURE1:7; :: thesis: verum
end;
suppose A2: a = -infty ; :: thesis: I in Borel_Sets
then A3: a < b by XREAL_0:def 1, XXREAL_0:12;
].a,b.[ is Element of Borel_Sets by A2, FINANCE1:3;
then ( ].a,b.[ in Borel_Sets & {b} in Borel_Sets ) by FINANCE2:5;
then ].a,b.[ \/ {b} in Borel_Sets by MEASURE1:11;
hence I in Borel_Sets by A1, A3, XXREAL_1:132; :: thesis: verum
end;
suppose a in REAL ; :: thesis: I in Borel_Sets
then I is Element of Borel_Sets by A1, FINANCE2:6;
hence I in Borel_Sets ; :: thesis: verum
end;
end;