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 4 :: 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