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 8 :: thesis: ex b being real number st ].-infty ,1.] = ].-infty ,b.]
take 1 ; :: thesis: ].-infty ,1.] = ].-infty ,1.]
thus ].-infty ,1.] = ].-infty ,1.] ; :: thesis: verum