take [.0 ,+infty .[ ; :: thesis: ( not [.0 ,+infty .[ is empty & [.0 ,+infty .[ is right_open_interval )
0 in [.0 ,+infty .[ by XXREAL_1:236;
hence not [.0 ,+infty .[ is empty ; :: thesis: [.0 ,+infty .[ is right_open_interval
take 0 ; :: according to MEASURE5:def 7 :: thesis: ex b being R_eal st [.0 ,+infty .[ = [.0 ,b.[
take +infty ; :: thesis: [.0 ,+infty .[ = [.0 ,+infty .[
thus [.0 ,+infty .[ = [.0 ,+infty .[ ; :: thesis: verum