take
].-infty,1.]
; :: thesis: ( not ].-infty,1.] is empty & ].-infty,1.] is left_open_interval )

1 in ].-infty,1.] by XXREAL_1:234;

hence not ].-infty,1.] is empty ; :: thesis: ].-infty,1.] is left_open_interval

take -infty ; :: according to MEASURE5:def 5 :: thesis: ex b being Real st ].-infty,1.] = ].-infty,b.]

take 1 ; :: thesis: ].-infty,1.] = ].-infty,1.]

thus ].-infty,1.] = ].-infty,1.] ; :: thesis: verum

1 in ].-infty,1.] by XXREAL_1:234;

hence not ].-infty,1.] is empty ; :: thesis: ].-infty,1.] is left_open_interval

take -infty ; :: according to MEASURE5:def 5 :: thesis: ex b being Real st ].-infty,1.] = ].-infty,b.]

take 1 ; :: thesis: ].-infty,1.] = ].-infty,1.]

thus ].-infty,1.] = ].-infty,1.] ; :: thesis: verum