for a, b being Real holds Intersection (half_open_sets (a,b)) is Element of Borel_Sets