reconsider Set1 = ExtREAL as Element of Ext_Borel_Sets by PROB_1:23;
reconsider Set2 = {+infty} as Element of Ext_Borel_Sets by Th5000, Th6000;
reconsider Set3 = {-infty} as Element of Ext_Borel_Sets by Th500, Th600;
reconsider Set4 = Set1 \ Set2 as Element of Ext_Borel_Sets ;
Set4 = [.-infty,+infty.[ \/ ].+infty,+infty.] by XXREAL_1:388, XXREAL_1:209
.= [.-infty,+infty.[ ;
then PP: Set4 \ Set3 = [.-infty,-infty.[ \/ ].-infty,+infty.[ by XXREAL_1:387
.= ].-infty,+infty.[ ;
reconsider Set5 = Set4 \ Set3 as Element of Ext_Borel_Sets ;
thus REAL is Element of Ext_Borel_Sets by XXREAL_1:224, PP; :: thesis: verum