theorem Th5000: :: FINANCE5:19

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