environ
vocabularies HIDDEN, NUMBERS, INT_1, SUBSET_1, XXREAL_0, FINSET_1, ARYTM_3, XBOOLE_0, ARYTM_1, NAT_1, FUNCT_1, RELAT_1, TARSKI, ORDINAL1, MEMBERED, ORDINAL2, FINSUB_1, SETWISEO, CARD_1, XREAL_0, RAT_1, XXREAL_1, XXREAL_2, MEASURE5, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, CARD_1, FINSUB_1, SETWISEO, NUMBERS, MEMBERED, XXREAL_0, XCMPLX_0, XREAL_0, INT_1, NAT_1, RAT_1, XXREAL_1;
definitions TARSKI, MEMBERED;
theorems XXREAL_0, MEMBERED, TARSKI, XBOOLE_0, XXREAL_1, XBOOLE_1, FINSUB_1, XREAL_0, XREAL_1, INT_1, NAT_1, FINSET_1, ZFMISC_1, FUNCT_1, SETFAM_1;
schemes XXREAL_1, NAT_1, SETWISEO, CLASSES1;
registrations XXREAL_0, MEMBERED, XXREAL_1, XBOOLE_0, FINSET_1, NUMBERS, SETWISEO, FINSUB_1, XREAL_0, INT_1, NAT_1, CARD_1, ORDINAL1;
constructors HIDDEN, XXREAL_0, MEMBERED, XREAL_0, INT_1, FINSET_1, RAT_1, XXREAL_1, SETWISEO, XCMPLX_0, REAL_1, NAT_1, XTUPLE_0, CARD_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities ORDINAL1;
expansions ;
Lm1:
for x being ExtReal holds sup {x} = x
Lm2:
for x being ExtReal holds inf {x} = x
Lm3:
for x, y being ExtReal st x <= y holds
y is UpperBound of {x,y}
Lm4:
for x, y being ExtReal
for z being UpperBound of {x,y} holds y <= z
Lm5:
for x, y being ExtReal st y <= x holds
y is LowerBound of {x,y}
Lm6:
for x, y being ExtReal
for z being LowerBound of {x,y} holds z <= y