now

let xt be Point of (LinearTopSpaceNorm X); :: thesis: ex Bt being Basis of xt st Bt is countable
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
consider B being Basis of x such that
A1: B is countable by FRECHET:def 1;
B is Subset-Family of (LinearTopSpaceNorm X) by Def4;
then reconsider Bt = B as Basis of xt by Th25;
take Bt = Bt; :: thesis: Bt is countable
thus Bt is countable by A1; :: thesis: verum

end;

hence LinearTopSpaceNorm X is first-countable by FRECHET:def 1; :: thesis: verum