begin
Lm1:
for T being non empty TopSpace st ( for p being Point of 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 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 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
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
Lm5:
for T being non empty TopSpace st T is first-countable holds
for x being Point of 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 ) )
theorem
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem
begin
theorem Th14:
theorem
begin
:: deftheorem FRECHET2:def 1 :
canceled;
:: deftheorem Def2 defines Cl_Seq FRECHET2:def 2 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
begin
:: deftheorem Def3 defines lim FRECHET2:def 3 :
theorem Th27:
theorem Th28:
theorem
theorem
theorem Th31:
theorem
theorem
begin
:: deftheorem Def4 defines is_a_cluster_point_of FRECHET2:def 4 :
theorem Th34:
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
canceled;
theorem Th43:
theorem Th44:
theorem
begin
theorem
theorem
theorem
theorem