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;