theorem Th5: :: FINANCE1:5

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