let T be TopSpace; ( T is empty implies T is metrizable )
set cT = the carrier of T;
A1:
( dom {} = {} & rng {} c= REAL )
by XBOOLE_1:2;
assume A2:
T is empty
; 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: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
; PCOMPS_1:def 9 ( E is_metric_of the carrier of T & Family_open_set (SpaceMetr the carrier of T,E) = the topology of T )
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) )
proof
let a,
b,
c be
Element of the
carrier of
T;
( ( 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) )
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;
verum
end;
hence
E is_metric_of the carrier of T
by PCOMPS_1:def 7; Family_open_set (SpaceMetr the carrier of T,E) = the topology of T
then A5:
SpaceMetr the carrier of T,E = MetrStruct(# the carrier of T,E #)
by PCOMPS_1:def 8;
then
the carrier of T in Family_open_set (SpaceMetr the carrier of T,E)
by PCOMPS_1:34;
then
Family_open_set (SpaceMetr the carrier of T,E) = {{} }
by A3, A5, ZFMISC_1:39;
hence
Family_open_set (SpaceMetr the carrier of T,E) = the topology of T
by A3, ZFMISC_1:39; verum