consider a, b being R_eal;
take [.0 ,+infty .[ ; :: thesis: [.0 ,+infty .[ is right_open_interval
take 0 ; :: according to MEASURE5:def 7 :: thesis: ex b being R_eal st
( 0 <= b & [.0 ,+infty .[ = [.0 ,b.[ )
take +infty ; :: thesis: ( 0 <= +infty & [.0 ,+infty .[ = [.0 ,+infty .[ )
thus ( 0 <= +infty & [.0 ,+infty .[ = [.0 ,+infty .[ ) ; :: thesis: verum