for a, b being Real
for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets