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

proof

set L = halfline k;
FG2: ( halfline k in Family_of_halflines & halfline k = ].-infty,k.[ ) by A;
Family_of_halflines c= sigma Family_of_halflines by PROB_1:def 9;
hence ].-infty,k.[ in Borel_Sets by FG2; :: 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 AJF0, FJ20; :: thesis: verum