take [.0 ,1.] ; :: thesis: ( not [.0 ,1.] is empty & [.0 ,1.] is closed_interval )
thus not [.0 ,1.] is empty by XXREAL_1:30; :: thesis: [.0 ,1.] is closed_interval
take 0 ; :: according to MEASURE5:def 6 :: thesis: ex b being real number st [.0 ,1.] = [.0 ,b.]
take 1 ; :: thesis: [.0 ,1.] = [.0 ,1.]
thus [.0 ,1.] = [.0 ,1.] ; :: thesis: verum