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

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