for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )