environ
vocabularies HIDDEN, NUMBERS, METRIC_1, PRE_TOPC, REAL_1, XBOOLE_0, TARSKI, COMPLEX1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, NAT_1, SETFAM_1, FINSEQ_1, TOPMETR, RELAT_1, FINSET_1, FUNCT_1, ORDINAL2, RCOMP_1, SUBSET_1, ZFMISC_1, EUCLID, XXREAL_2, STRUCT_0, PCOMPS_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, WEIERSTR;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, TOPMETR, METRIC_1, COMPTS_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, FINSEQ_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_2, RCOMP_1, EUCLID, PCOMPS_1, XXREAL_0, XXREAL_2;
definitions TARSKI, XXREAL_2;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, FINSEQ_1, ZFMISC_1, SEQ_2, SEQ_4, ABSVALUE, COMPTS_1, RELAT_1, TOPS_2, RCOMP_1, TOPMETR, PCOMPS_1, METRIC_1, METRIC_6, XBOOLE_0, XBOOLE_1, XREAL_0, SUBSET_1, XREAL_1, COMPLEX1, XXREAL_0, SETFAM_1;
schemes NAT_1, SUBSET_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, FINSEQ_1, NAT_1;
constructors HIDDEN, REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, TOPS_2, COMPTS_1, EUCLID, TOPMETR, BINOP_2, PCOMPS_1, COMSEQ_2, BINOP_1;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities STRUCT_0;
expansions TARSKI, XXREAL_2;
Lm1:
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
Lm2:
[#] R^1 <> {}
;
:: The Weierstrass` theorem
::