environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, RCOMP_1, TARSKI, NAT_1, NUMBERS, FUNCOP_1, FRECHET, SUBSET_1, CARD_1, STRUCT_0, ORDINAL2, RELAT_1, SEQ_1, VALUED_0, XXREAL_0, FUNCT_1, RLVECT_3, CARD_3, SETFAM_1, ORDINAL1, ZFMISC_1, FINSET_1, ARYTM_3, SEQ_2, METRIC_1, PCOMPS_1, METRIC_6, XREAL_0, REAL_1, WAYBEL_7, ARYTM_1, FUNCT_2, FRECHET2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SETFAM_1, FINSET_1, CARD_3, TOPS_2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, SEQ_1, FUNCT_2, NAT_1, XXREAL_2, VALUED_0, METRIC_1, PCOMPS_1, TBSP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, FUNCOP_1, METRIC_6, YELLOW_8, FRECHET, SEQ_4;
definitions TARSKI, SEQM_3, PRE_TOPC, TOPS_2, METRIC_6, FUNCT_1, FRECHET, XBOOLE_0;
theorems FRECHET, URYSOHN1, YELLOW_8, PRE_TOPC, TARSKI, FUNCOP_1, NORMSP_1, ZFMISC_1, PCOMPS_1, FUNCT_1, AXIOMS, CARD_1, RELAT_1, SETFAM_1, ORDINAL1, FUNCT_2, TOPS_2, SUBSET_1, SEQM_3, NAT_1, INT_1, SEQ_1, TOPMETR, METRIC_6, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, VALUED_0, XXREAL_2, CARD_3;
schemes CLASSES1, DOMAIN_1, NAT_1, RECDEF_1, SEQ_1, FUNCT_1, VALUED_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, FRECHET, VALUED_0, CARD_1, XXREAL_2, ORDINAL1, FINSET_1, NAT_1;
constructors HIDDEN, SETFAM_1, REALSET1, CARD_3, TOPS_2, TBSP_1, METRIC_6, YELLOW_8, FRECHET, SEQ_4, RELSET_1, FUNCOP_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, CARD_1, ORDINAL1;
expansions TARSKI, PRE_TOPC, TOPS_2, METRIC_6, FUNCT_1, FRECHET, XBOOLE_0;
Lm1:
for T being non empty TopSpace st ( for p being Point of T holds Cl {p} = {p} ) holds
T is T_1
Lm2:
for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
Lm3:
for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
Lm4:
for T being non empty TopSpace st T is T_2 holds
T is T_1
Lm5:
for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )