let k be Real; :: thesis: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )
A1: k in REAL by XREAL_0:def 1;
set R = ].-infty,k.[;
A2: ].-infty,k.[ in Borel_Sets

proof

set L = halfline k;
A3: ( halfline k in Family_of_halflines & halfline k = ].-infty,k.[ ) by A1;
Family_of_halflines c= sigma Family_of_halflines by PROB_1:def 9;
hence ].-infty,k.[ in Borel_Sets by A3; :: thesis: verum

end;

then ].-infty,k.[ ` in Borel_Sets by PROB_1:def 1;
hence ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th2, A2; :: thesis: verum