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