take ].-infty,+infty.[ ; :: thesis: ( not ].-infty,+infty.[ is empty & ].-infty,+infty.[ is open_interval )
In (0,REAL) 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 2 :: 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