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