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 3 :: thesis: ex b being Real st [.0,1.] = [.0,b.]
take 1 ; :: thesis: [.0,1.] = [.0,1.]
thus [.0,1.] = [.0,1.] ; :: thesis: verum