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₁ being Element of Borel_Sets holds b₁ is empty by A3, A2; :: thesis: verum