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 b₁ being Element of K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))) holds
( not b₁ c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or union b₁ in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) & ( for b₁, b₂ being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds
( not b₁ in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b₂ in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b₁ /\ b₂ 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 b₁, b₂ being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds
( not b₁ in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b₂ in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b₁ /\ b₂ 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