let k be Real; :: thesis: ( ].k,+infty.] is Element of Ext_Borel_Sets & [.-infty,k.] is Element of Ext_Borel_Sets )
A3: [.-infty,k.] in Ext_Family_of_halflines ;
a2: Ext_Family_of_halflines c= sigma Ext_Family_of_halflines by PROB_1:def 9;
ExtREAL in Ext_Borel_Sets by PROB_1:5;
then ExtREAL \ [.-infty,k.] in Ext_Borel_Sets by a2, PROB_1:6, A3;
hence ( ].k,+infty.] is Element of Ext_Borel_Sets & [.-infty,k.] is Element of Ext_Borel_Sets ) by Th2, a2, A3; :: thesis: verum