let I be Subset of REAL; :: thesis: ( I is closed_interval implies I in Borel_Sets )
assume I is closed_interval ; :: thesis: I in Borel_Sets
then consider a, b being Real such that
A1: I = [.a,b.] by MEASURE5:def 3;
A2: ( ].a,b.] is Element of Borel_Sets & {a} is Element of Borel_Sets ) by FINANCE2:5, FINANCE2:6;
per cases ( a <= b or a > b ) ;
suppose a <= b ; :: thesis: I in Borel_Sets
then I = ].a,b.] \/ {a} by A1, XXREAL_1:130;
hence I in Borel_Sets by A2, MEASURE1:11; :: thesis: verum
end;
suppose a > b ; :: thesis: I in Borel_Sets
then I = {} by A1, XXREAL_1:29;
hence I in Borel_Sets by MEASURE1:7; :: thesis: verum
end;
end;