theorem Th500: :: FINANCE5:16

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