let T be TopSpace; :: thesis:
set cT = the carrier of T;
A1: ( dom {} = {} & rng {} c= REAL ) by XBOOLE_1:2;
assume A2: T is empty ; :: thesis:
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:113;
then reconsider E = {} as Function of [: the carrier of T, the carrier of T:],REAL by A1, FUNCT_2:4;
set M = SpaceMetr ( the carrier of T,E);
take E ; :: according to PCOMPS_1:def 9 :: thesis:
for a, b, c being Element of the carrier of T holds
( ( E . (a,b) = 0 implies a = b ) & ( a = b implies E . (a,b) = 0 ) & E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) )

let a, b, c be Element of the carrier of T; :: thesis:
not [{},{}] in dom E ;
then A4: E . ({},{}) = {} by FUNCT_1:def 4;
( a = {} & b = {} ) by A2, SUBSET_1:def 2;
hence ( ( E . (a,b) = 0 implies a = b ) & ( a = b implies E . (a,b) = 0 ) & E . (a,b) = E . (b,a) & E . (a,c) <= (E . (a,b)) + (E . (b,c)) ) by A4; :: thesis:

end;