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

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