A Finite_space is a Maths_space that has a finite number of members and that has all its members enumerated by an implementation of this part of ISO 10303.
NOTE - A Finite_integer_interval has a finite number of members, but is not a Finite_space according to the definition above unless you enumerate them.
EXPRESS specification:
*) ENTITY Finite_space SUBTYPE OF (Maths_space); members : SET [0,?] OF Maths_value; END_ENTITY; (*
Attributes:
members The members of the Finite_space.