let X be set ; for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ) holds
ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
let O be Subset-Family of (bool X); ( ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ) implies ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) ) )
assume A1:
for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace
; ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
reconsider B = Intersect O as Subset-Family of X ;
set T = TopStruct(# X,B #);
take
B
; ( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
thus
B = Intersect O
; ( TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
A2:
TopStruct(# X,B #) is TopSpace-like
proof
hence
the
carrier of
TopStruct(#
X,
B #)
in the
topology of
TopStruct(#
X,
B #)
by SETFAM_1:43;
PRE_TOPC:def 1 ( ( for b1 being Element of K32(K32( the carrier of TopStruct(# X,B #))) holds
( not b1 c= the topology of TopStruct(# X,B #) or union b1 in the topology of TopStruct(# X,B #) ) ) & ( for b1, b2 being Element of K32( the carrier of TopStruct(# X,B #)) holds
( not b1 in the topology of TopStruct(# X,B #) or not b2 in the topology of TopStruct(# X,B #) or b1 /\ b2 in the topology of TopStruct(# X,B #) ) ) )
let a,
b be
Subset of
TopStruct(#
X,
B #);
( not a in the topology of TopStruct(# X,B #) or not b in the topology of TopStruct(# X,B #) or a /\ b in the topology of TopStruct(# X,B #) )
assume that A7:
a in the
topology of
TopStruct(#
X,
B #)
and A8:
b in the
topology of
TopStruct(#
X,
B #)
;
a /\ b in the topology of TopStruct(# X,B #)
hence
a /\ b in the
topology of
TopStruct(#
X,
B #)
by SETFAM_1:43;
verum
end;
hence
TopStruct(# X,B #) is TopSpace
; ( ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
thus
for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #)
for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of Tproof
let o be
Subset-Family of
X;
( o in O implies TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) )
assume A12:
o in O
;
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #)
reconsider S =
TopStruct(#
X,
o #) as
TopSpace by A1, A12;
Intersect O c= o
by A12, MSSUBFAM:2;
then
S is
TopExtension of
TopStruct(#
X,
B #)
by YELLOW_9:def 5;
hence
TopStruct(#
X,
o #) is
TopExtension of
TopStruct(#
X,
B #)
;
verum
end;
reconsider TT = TopStruct(# X,B #) as TopSpace by A2;
let T9 be TopSpace; ( the carrier of T9 = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T9 ) implies TopStruct(# X,B #) is TopExtension of T9 )
assume that
A13:
the carrier of T9 = X
and
A14:
for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T9
; TopStruct(# X,B #) is TopExtension of T9
then
the topology of T9 c= Intersect O
by A13, MSSUBFAM:4;
then
TT is TopExtension of T9
by A13, YELLOW_9:def 5;
hence
TopStruct(# X,B #) is TopExtension of T9
; verum