for r being Real
for X being non empty interval Subset of REAL holds
( r in X or r <= lower_bound X or upper_bound X <= r )