take
].-infty,+infty.[
; ( 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
; ].-infty,+infty.[ is open_interval
take
-infty
; MEASURE5:def 2 ex b being R_eal st ].-infty,+infty.[ = ].-infty,b.[
take
+infty
; ].-infty,+infty.[ = ].-infty,+infty.[
thus
].-infty,+infty.[ = ].-infty,+infty.[
; verum