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

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