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 A1: 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 2 :: thesis: ex b₁ being Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) st b₁ is countable
reconsider y = x as Point of T ;
consider C being Basis of such that
A2: C is countable by A1;
reconsider B = C as Basis of by Lm1;
take B ; :: thesis: B is countable
thus B is countable by A2; :: thesis: verum

end;

assume A3: 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 2 :: thesis: ex b₁ being Element of bool (bool the carrier of T) st b₁ is countable
reconsider y = x as Point of TopStruct(# the carrier of T, the topology of T #) ;
consider C being Basis of such that
A4: C is countable by A3;
reconsider B = C as Basis of by Lm1;
take B ; :: thesis: B is countable
thus B is countable by A4; :: thesis: verum