for X being interval Subset of REAL st not X is bounded_above & not X is bounded_below holds
X = REAL