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

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