let M be non empty MetrSpace; :: thesis: TopSpaceMetr M is first-countable
let x be Point of (TopSpaceMetr M); :: according to FRECHET:def 1 :: thesis: ex B being Basis of x st B is countable
reconsider x' = x as Element of (TopSpaceMetr M) ;
reconsider x' = x' as Element of M by TOPMETR:16;
reconsider x' = x' as Point of M ;
consider B being Basis of x such that
B = { (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } and
A1: B is countable and
ex f being Function of NAT ,B st
for n being set st n in NAT holds
ex n' being Element of NAT st
( n = n' & f . n = Ball x',(1 / (n' + 1)) ) by Th11;
take B ; :: thesis: B is countable
thus B is countable by A1; :: thesis: verum