let k1, k2 be Real; :: thesis: [.k2,k1.[ is Element of Borel_Sets
set R = ].-infty,k2.[;
( k1 in REAL & k2 in REAL ) by XREAL_0:def 1;
then A1: ( -infty < k2 & k1 < +infty ) by XXREAL_0:9, XXREAL_0:12;
A2: REAL \ ].-infty,k2.[ = [.k2,+infty.[ by Th2;
( ].-infty,k2.[ ` is Element of Borel_Sets & ].-infty,k1.[ is Element of Borel_Sets & [.k1,+infty.[ is Element of Borel_Sets ) by Th3, A2;
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 Th2;
hence [.k2,k1.[ is Element of Borel_Sets by A1, XXREAL_1:154; :: thesis: verum