A Real_interval is a Maths_space that is the set of all reals defined by a lower bound, and upper bound or both.
EXPRESS specification:
*) ENTITY Real_interval ABSTRACT SUPERTYPE OF (ONEOF ( Finite_real_interval, Hibounded_real_interval, Lobounded_real_interval)) SUBTYPE OF (Maths_space); END_ENTITY; (*