consider a, b being R_eal such that
A1: ( a = -infty & b = +infty ) ;
take ].a,b.[ ; :: thesis: ].a,b.[ is open_interval
take a ; :: according to MEASURE5:def 5 :: thesis: ex b being R_eal st
( a <= b & ].a,b.[ = ].a,b.[ )
take b ; :: thesis: ( a <= b & ].a,b.[ = ].a,b.[ )
thus ( a <= b & ].a,b.[ = ].a,b.[ ) by A1; :: thesis: verum