environ
vocabularies HIDDEN, NUMBERS, FREEALG, SETFAM_1, CARD_1, XBOOLE_0, SUBSET_1, REAL_1, ORDINAL1, TARSKI, FUNCT_1, RELAT_1, ZFMISC_1, ARYTM_3, XXREAL_0, ARYTM_1, SEQ_1, SEQ_2, VALUED_0, ORDINAL2, XXREAL_2, SEQ_4, RCOMP_1, XXREAL_1, MEMBER_1, FUNCOP_1, PRALG_1, PRE_TOPC, STRUCT_0, LIMFUNC1, EUCLID, MCART_1, RLTOPSP1, PSCOMP_1, FUNCT_7, XCMPLX_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, SETFAM_1, REAL_1, NAT_1, INT_1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_2, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, LIMFUNC1, COMPTS_1, RLTOPSP1, EUCLID, XXREAL_0, XXREAL_2, MEASURE6;
definitions TARSKI, TOPS_2, ORDINAL1, XXREAL_2, SEQ_2, MEASURE6;
theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, SEQ_4, RCOMP_1, FUNCOP_1, EUCLID, SEQ_1, SEQ_2, TOPS_1, TSP_1, COMPTS_1, SETFAM_1, ZFMISC_1, TOPREAL1, JORDAN1, GOBOARD7, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, MEASURE6, XREAL_1, XXREAL_0, VALUED_1, XXREAL_2, RLTOPSP1, XXREAL_1, MEMBER_1, ORDINAL1;
schemes FUNCT_2, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, SEQ_2, STRUCT_0, PRE_TOPC, COMPTS_1, EUCLID, SPPOL_2, VALUED_0, VALUED_1, XXREAL_2, FINSET_1, FCONT_3, MEASURE6, TOPREAL1, RELSET_1, XCMPLX_0;
constructors HIDDEN, DOMAIN_1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, FUNCOP_1, LIMFUNC1, MEASURE6, TOPS_2, COMPTS_1, PCOMPS_1, TSP_1, TOPREAL1, SUPINF_1, XXREAL_2, PARTFUN1, RELSET_1, BINOP_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RCOMP_1, STRUCT_0, SUBSET_1, LIMFUNC1, XCMPLX_0, MEASURE6;
expansions TARSKI, RCOMP_1, XXREAL_2, MEASURE6;
Lm1:
for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
Lm2:
for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max
Lm3:
for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )