consider m being Real such that

A1: m > -infty ;

set L = halfline m;

set LL = Family_of_halflines ;

A2: not halfline m is empty by A1, XXREAL_1:33;

m in REAL by XREAL_0:def 1;

then A3: halfline m in Family_of_halflines ;

Family_of_halflines is Subset of Borel_Sets by PROB_1:def 9;

hence not for b_{1} being Element of Borel_Sets holds b_{1} is empty
by A3, A2; :: thesis: verum

A1: m > -infty ;

set L = halfline m;

set LL = Family_of_halflines ;

A2: not halfline m is empty by A1, XXREAL_1:33;

m in REAL by XREAL_0:def 1;

then A3: halfline m in Family_of_halflines ;

Family_of_halflines is Subset of Borel_Sets by PROB_1:def 9;

hence not for b