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

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 ) by A7;
then T is normal by PRE_TOPC:def 18;
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;
A9: t is T_1 by NAGATA_2:19;
( t is regular & ex Bn being FamilySequence of t st Bn is Basis_sigma_locally_finite ) by NAGATA_2:19;
then T is normal by A9, NAGATA_1:20;
hence T is T_4 by A9; :: thesis: verum

end;

end;