reconsider e = {} (bool {}), tE = {({} {})} as Subset-Family of {} ;
reconsider E = {} (bool (bool {})) as empty Subset-Family of (bool {}) ;
let X be set ; for O being Subset-Family of (bool X) ex B being Subset-Family of X st
( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
let O be Subset-Family of (bool X); ex B being Subset-Family of X st
( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
reconsider B = UniCl (FinMeetCl (union O)) as Subset-Family of X ;
take
B
; ( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
thus
B = UniCl (FinMeetCl (union O))
; ( TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
reconsider dT = TopStruct(# {},tE #) as discrete TopStruct by TDLAT_3:def 1, ZFMISC_1:1;
A1:
{{},{}} = tE
by ENUMSET1:29;
A2:
FinMeetCl tE = {{},{}}
by YELLOW_9:11;
hence
TopStruct(# X,B #) is TopSpace
by CANTOR_1:15; ( ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
reconsider TT = TopStruct(# X,B #) as TopSpace by A3, CANTOR_1:15;
let T be TopSpace; ( the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) implies T is TopExtension of TopStruct(# X,B #) )
assume that
A8:
the carrier of T = X
and
A9:
for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #)
; T is TopExtension of TopStruct(# X,B #)
thus
the carrier of T = the carrier of TopStruct(# X,B #)
by A8; YELLOW_9:def 5 the topology of TopStruct(# X,B #) c= the topology of T
A10:
( X <> {} implies not T is empty )
by A8;
then
union O c= the topology of T
by ZFMISC_1:76;
then
FinMeetCl (union O) c= FinMeetCl the topology of T
by A8, CANTOR_1:14;
then A12:
B c= UniCl (FinMeetCl the topology of T)
by A8, CANTOR_1:9;
X in the topology of T
by A8, PRE_TOPC:def 1;
hence
the topology of TopStruct(# X,B #) c= the topology of T
by A12, A10, CANTOR_1:7; verum