let M be non empty MetrSpace; :: thesis: TopSpaceMetr M is first-countable
let x be Point of (TopSpaceMetr M); :: according to FRECHET:def 2 :: thesis: ex B being Basis of x st B is countable
take Balls x ; :: thesis: Balls x is countable
thus Balls x is countable ; :: thesis: verum