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

hence ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th2, A2; :: thesis: verum

A1: k in REAL by XREAL_0:def 1;

set R = ].-infty,k.[;

A2: ].-infty,k.[ in Borel_Sets

proof

then
].-infty,k.[ ` in Borel_Sets
by PROB_1:def 1;
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;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

hence ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th2, A2; :: thesis: verum