set T = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is TopSpace-like
proof
reconsider z = COMPLEX n as Subset of (COMPLEX n) by ZFMISC_1:def 1;
z is open by SEQ_4:107;
hence the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))) holds
( not b1 c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or union b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) & ( for b1, b2 being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds
( not b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b1 /\ b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) )
thus for A being Subset-Family of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) st A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) holds
union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) :: thesis: for b1, b2 being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds
( not b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b1 /\ b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) )
proof
let A be Subset-Family of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); :: thesis: ( A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) implies union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) )
assume A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; :: thesis: union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)
then A1: for B being Subset of (COMPLEX n) st B in A holds
B is open by SEQ_4:131;
reconsider z = union A as Subset of (COMPLEX n) ;
z is open by A1, SEQ_4:108;
hence union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; :: thesis: verum
end;
let A, B be Subset of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); :: thesis: ( not A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) )
reconsider z1 = A, z2 = B as Subset of (COMPLEX n) ;
reconsider z = A /\ B as Subset of (COMPLEX n) ;
assume ( A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) & B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ; :: thesis: A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)
then ( z1 is open & z2 is open ) by SEQ_4:131;
then z is open by SEQ_4:109;
hence A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; :: thesis: verum
end;
hence TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace ; :: thesis: verum