environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, XXREAL_0, MEMBERED, XXREAL_2, ORDINAL1, XBOOLE_0, TARSKI, ORDINAL2, SETFAM_1, SUPINF_1;
notations HIDDEN, XBOOLE_0, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XXREAL_2;
definitions MEMBERED, SETFAM_1;
theorems TARSKI, XXREAL_0, SETFAM_1, XXREAL_2;
schemes MEMBERED;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, MEMBERED;
constructors HIDDEN, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, SETFAM_1, DOMAIN_1, XXREAL_2;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions MEMBERED;
:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL
::