let T be TopSpace; :: thesis: ( T is empty implies T is metrizable )
set cT = the carrier of T;
A1: ( dom {} = {} & rng {} c= REAL ) ;
assume A2: T is empty ; :: thesis: T is metrizable
then A3: bool the carrier of T = {{}} by ZFMISC_1:1;
the carrier of T = {} by A2;
then [: the carrier of T, the carrier of T:] = {} by ZFMISC_1:90;
then reconsider E = {} as Function of [: the carrier of T, the carrier of T:],REAL by A1, FUNCT_2:2;
set M = SpaceMetr ( the carrier of T,E);
take E ; :: according to PCOMPS_1:def 8 :: thesis: ( E is_metric_of the carrier of T & Family_open_set (SpaceMetr ( the carrier of T,E)) = the topology of T )
thus E is_metric_of the carrier of T :: thesis: Family_open_set (SpaceMetr ( the carrier of T,E)) = the topology of T

proof

let a, b, c be Element of the carrier of T; :: according to PCOMPS_1:def 6 :: thesis: ( ( not E . (a,b) = 0 or a = b ) & ( not a = b or E . (a,b) = 0 ) & E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) )
A4: ( a = 0 & b = 0 ) by A2, SUBSET_1:def 1;
thus ( E . (a,b) = 0 iff a = b ) by A4; :: thesis: ( E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) )
thus E . (a,b) = E . (b,a) by A4; :: thesis: E . (a,c) <= (E . (a,b)) + (E . (b,c))
E . (a,b) = 0 ;
hence E . (a,c) <= (E . (a,b)) + (E . (b,c)) ; :: thesis: verum

end;

then A5: SpaceMetr ( the carrier of T,E) = MetrStruct(# the carrier of T,E #) by PCOMPS_1:def 7;
then the carrier of T in Family_open_set (SpaceMetr ( the carrier of T,E)) by PCOMPS_1:30;
then Family_open_set (SpaceMetr ( the carrier of T,E)) = {{}} by A3, A5, ZFMISC_1:33;
hence Family_open_set (SpaceMetr ( the carrier of T,E)) = the topology of T by A3, ZFMISC_1:33; :: thesis: verum