theorem Th50: :: FINANCE5:11

for b being Real holds Intersection (ext_half_open_sets b) is Element of Ext_Borel_Sets