let r be Real; :: thesis: [.r,+infty.] is Event of Ext_Borel_Sets
Intersection (ext_half_open_sets r) is Element of Ext_Borel_Sets by Th50;
hence [.r,+infty.] is Event of Ext_Borel_Sets by Th60; :: thesis: verum