let T be non empty TopSpace; :: thesis: ( T is first-countable iff Chi T c= omega )
set X = { (Chi (x,T)) where x is Point of T : verum } ;
A1: Chi T = union { (Chi (x,T)) where x is Point of T : verum } by Th4;
thus ( T is first-countable implies Chi T c= omega ) :: thesis: ( Chi T c= omega implies T is first-countable )
proof
assume A2: for x being Point of T ex B being Basis of x st B is countable ; :: according to FRECHET:def 2 :: thesis: Chi T c= omega
now :: thesis: for a being set st a in { (Chi (x,T)) where x is Point of T : verum } holds
a c= omega
let a be set ; :: thesis: ( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= omega )
assume a in { (Chi (x,T)) where x is Point of T : verum } ; :: thesis: a c= omega
then consider x being Point of T such that
A3: a = Chi (x,T) ;
consider B being Basis of x such that
A4: B is countable by A2;
A5: card B c= omega by A4;
Chi (x,T) c= card B by Def1;
hence a c= omega by A3, A5; :: thesis: verum
end;
hence Chi T c= omega by A1, ZFMISC_1:76; :: thesis: verum
end;
assume A6: Chi T c= omega ; :: thesis: T is first-countable
let x be Point of T; :: according to FRECHET:def 2 :: thesis: ex b1 being Element of K32(K32( the carrier of T)) st b1 is countable
consider B being Basis of x such that
A7: Chi (x,T) = card B by Def1;
take B ; :: thesis: B is countable
Chi (x,T) c= Chi T by Th5;
hence card B c= omega by A6, A7; :: according to CARD_3:def 14 :: thesis: verum