consider a, b being R_eal such that
A2: ( a = -infty & b = +infty ) ;
take ].a,1.] ; :: thesis: ].a,1.] is left_open_interval
take a ; :: according to MEASURE5:def 8 :: thesis: ex b being real number st
( a <= b & ].a,1.] = ].a,b.] )
take 1 ; :: thesis: ( a <= 1 & ].a,1.] = ].a,1.] )
thus ( a <= 1 & ].a,1.] = ].a,1.] ) by A2; :: thesis: verum