take [.0 ,1.] ; :: thesis: [.0 ,1.] is closed-interval
thus [.0 ,1.] is closed-interval by Def1; :: thesis: verum