environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, RELAT_1, SETFAM_1, TARSKI, XBOOLE_0, ZFMISC_1, PROB_1, SUBSET_1, STRUCT_0, CARD_3, ORDINAL2, NAT_1, ARYTM_3, CARD_1, XXREAL_0, SEQ_2, FINSEQ_1, EUCLID, TOPREAL1, RCOMP_1, PRE_TOPC, METRIC_1, REAL_1, COMPLEX1, ARYTM_1, SEQ_1, INT_1, PCOMPS_1, FRECHET, RLVECT_3, YELLOW_8, CONNSP_2, TOPS_1, JORDAN2C, XXREAL_2, VALUED_0, MCART_1, TOPREAL2, JORDAN9, GOBOARD9, WAYBEL_7, KURATO_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1, XXREAL_0, XREAL_0, REAL_1, SETFAM_1, XTUPLE_0, MCART_1, DOMAIN_1, KURATO_0, RELAT_1, FUNCT_1, INT_1, FINSEQ_1, RELSET_1, FUNCT_2, NAT_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, METRIC_1, TBSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, BORSUK_1, CARD_3, PROB_1, CONNSP_2, TOPREAL1, TOPREAL2, JORDAN2C, VALUED_0, GOBOARD9, YELLOW_8, FRECHET, FRECHET2, TOPRNS_1, JORDAN9;
definitions XBOOLE_0, TARSKI, FRECHET, YELLOW_8;
theorems FRECHET, METRIC_1, TOPREAL3, TOPMETR, CONNSP_2, GOBOARD6, XBOOLE_1, PRE_TOPC, SUBSET_1, NAT_1, FUNCT_2, RELSET_1, TOPRNS_1, XBOOLE_0, FUNCT_1, INT_1, SPPOL_1, TOPS_1, TOPREAL6, JORDAN2C, TBSP_1, METRIC_6, ZFMISC_1, RELAT_1, GOBRD14, SEQM_3, MCART_1, BORSUK_1, FRECHET2, XREAL_1, XXREAL_0, ORDINAL1, VALUED_0, EUCLID, YELLOW_8, TOPS_2, KURATO_0, TARSKI;
schemes XBOOLE_0, FUNCT_1, SUBSET_1;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, XREAL_0, NAT_1, INT_1, STRUCT_0, TOPS_1, METRIC_1, PCOMPS_1, BORSUK_1, MONOID_0, EUCLID, TOPREAL2, TOPREAL5, JORDAN2C, VALUED_0, PRE_TOPC, SPPOL_1, RELSET_1;
constructors HIDDEN, REAL_1, TOPS_1, BORSUK_1, TBSP_1, MONOID_0, TOPRNS_1, TOPREAL2, GOBOARD9, FUNCSDOM, FRECHET, JORDAN2C, FRECHET2, JORDAN9, YELLOW_8, TOPS_2, KURATO_0, XTUPLE_0, JORDAN11;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities XBOOLE_0, SUBSET_1, STRUCT_0, XCMPLX_0;
expansions XBOOLE_0, TARSKI, FRECHET, YELLOW_8;
Lm1:
for T being non empty TopSpace
for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )