let k1, k2 be real number ; :: thesis: [.k2,k1.[ is Element of Borel_Sets
set R = ].-infty,k2.[;
( k1 in REAL & k2 in REAL ) by XREAL_0:def 1;
then J31: ( -infty < k2 & k1 < +infty ) by XXREAL_0:9, XXREAL_0:12;
J4: REAL \ ].-infty,k2.[ = [.k2,+infty.[ by AJF0;
( ].-infty,k2.[ ` is Element of Borel_Sets & ].-infty,k1.[ is Element of Borel_Sets & [.k1,+infty.[ is Element of Borel_Sets ) by BJ1, J4;
then ].-infty,k1.[ /\ (].-infty,k2.[ `) is Element of Borel_Sets by FINSUB_1:def 2;
then ].-infty,k1.[ /\ [.k2,+infty.[ is Element of Borel_Sets by AJF0;
hence [.k2,k1.[ is Element of Borel_Sets by J31, XXREAL_1:154; :: thesis: verum