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