environ
vocabularies HIDDEN, NUMBERS, REAL_1, XBOOLE_0, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, SUBSET_1, RCOMP_1, RELAT_1, CONNSP_2, TOPS_1, FUNCT_1, ORDINAL2, METRIC_1, CARD_1, XXREAL_0, ARYTM_3, REALSET1, ZFMISC_1, XXREAL_1, COMPLEX1, ARYTM_1, PCOMPS_1, FINSET_1, BORSUK_1, TOPMETR, MEMBERED, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XCMPLX_0, XREAL_0, REAL_1, NAT_1, DOMAIN_1, RELAT_1, REALSET1, FUNCT_1, PARTFUN1, RELSET_1, XXREAL_0, FUNCT_2, FINSET_1, BINOP_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, PCOMPS_1, CONNSP_2, RCOMP_1, BORSUK_1, COMPLEX1;
definitions PRE_TOPC, TARSKI, TOPS_2, MEMBERED;
theorems ABSVALUE, BINOP_1, BORSUK_1, COMPTS_1, CONNSP_2, FINSET_1, FUNCT_1, FUNCT_2, METRIC_1, PCOMPS_1, PRE_TOPC, TARSKI, TOPS_1, TOPS_2, ZFMISC_1, TBSP_1, RELAT_1, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, SETFAM_1, XXREAL_1, XXREAL_2;
schemes FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, REALSET1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, METRIC_3, PCOMPS_1, XXREAL_2, BORSUK_1, BINOP_2, VALUED_0;
constructors HIDDEN, SETFAM_1, REAL_1, COMPLEX1, RCOMP_1, REALSET1, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, FINSET_1, MEMBERED, XXREAL_2, PCOMPS_1, BINOP_1, BINOP_2, VALUED_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, BINOP_1, REALSET1, PCOMPS_1, METRIC_1;
expansions PRE_TOPC, TARSKI, TOPS_2;
Lm1:
for M being MetrSpace holds MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
Lm2:
for a, b, r being Real st r >= 0 & a + r <= b holds
a <= b