consider a, b being R_eal;
take [.0 ,1.] ; :: thesis: [.0 ,1.] is closed_interval
take 0 ; :: according to MEASURE5:def 6 :: thesis: ex b being real number st
( 0 <= b & [.0 ,1.] = [.0 ,b.] )
take 1 ; :: thesis: ( 0 <= 1 & [.0 ,1.] = [.0 ,1.] )
thus ( 0 <= 1 & [.0 ,1.] = [.0 ,1.] ) ; :: thesis: verum