consider I being closed-interval Subset of REAL ;
take I ; :: thesis: I is closed-interval
thus I is closed-interval ; :: thesis: verum