let T be non empty TopSpace; :: thesis: ( T is first-countable iff TopStruct(# the carrier of T,the topology of T #) is first-countable )
thus ( T is first-countable implies TopStruct(# the carrier of T,the topology of T #) is first-countable ) :: thesis: ( TopStruct(# the carrier of T,the topology of T #) is first-countable implies T is first-countable )

proof

assume Z: T is first-countable ; :: thesis: TopStruct(# the carrier of T,the topology of T #) is first-countable
let x be Point of TopStruct(# the carrier of T,the topology of T #); :: according to FRECHET:def 1 :: thesis: ex b₁ being Basis of x st b₁ is countable
reconsider y = x as Point of T ;
consider C being Basis of y such that
W: C is countable by Z, FRECHET:def 1;
reconsider B = C as Basis of x by Lmx;
take B ; :: thesis: B is countable
thus B is countable by W; :: thesis: verum

end;

assume Z: TopStruct(# the carrier of T,the topology of T #) is first-countable ; :: 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
reconsider y = x as Point of TopStruct(# the carrier of T,the topology of T #) ;
consider C being Basis of y such that
W: C is countable by Z, FRECHET:def 1;
reconsider B = C as Basis of x by Lmx;
take B ; :: thesis: B is countable
thus B is countable by W; :: thesis: verum