set I = the closed-interval Subset of REAL;
take the closed-interval Subset of REAL ; :: thesis: the closed-interval Subset of REAL is closed-interval
thus the closed-interval Subset of REAL is closed-interval ; :: thesis: verum