take ].-infty ,+infty .[ ; :: thesis: ( not ].-infty ,+infty .[ is empty & ].-infty ,+infty .[ is open_interval )
0 in ].-infty ,+infty .[ by XXREAL_1:224;
hence not ].-infty ,+infty .[ is empty ; :: thesis: ].-infty ,+infty .[ is open_interval
take -infty ; :: according to MEASURE5:def 5 :: thesis: ex b being R_eal st ].-infty ,+infty .[ = ].-infty ,b.[
take +infty ; :: thesis: ].-infty ,+infty .[ = ].-infty ,+infty .[
thus ].-infty ,+infty .[ = ].-infty ,+infty .[ ; :: thesis: verum