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

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