let T be TopSpace; :: thesis: ( T is metrizable implies T is T_4 )
assume A6: T is metrizable ; :: thesis: T is T_4

per cases ( T is empty or not T is empty ) ;

suppose A7: T is empty ; :: thesis: T is T_4

then for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) ;
then T is normal ;
hence T is T_4 by A7; :: thesis: verum

end;

suppose not T is empty ; :: thesis: T is T_4

then reconsider t = T as non empty metrizable TopSpace by A6;
( t is regular & ex Bn being FamilySequence of t st Bn is Basis_sigma_locally_finite ) by NAGATA_2:19;
then ( t is T_1 & T is normal ) by NAGATA_1:20, NAGATA_2:19;
hence T is T_4 ; :: thesis: verum

end;

end;