for k being Real holds
( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )