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 1 :: thesis: Chi T c= omega

now

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;
( Chi x,T c= card B & card B c= omega ) by A4, Def1, CARD_3:def 15;
hence a c= omega by A3, XBOOLE_1:1; :: thesis: verum

end;

hence Chi T c= omega by A1, ZFMISC_1:94; :: thesis: verum

end;

assume A5: Chi T c= omega ; :: thesis: T is first-countable
let x be Point of T; :: according to FRECHET:def 1 :: thesis: ex b₁ being Basis of x st b₁ is countable
consider B being Basis of x such that
A6: 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 A5, A6, XBOOLE_1:1; :: according to CARD_3:def 15 :: thesis: verum