set t = { A where A is Subset of D : union A in the topology of X } ;
{ A where A is Subset of D : union A in the topology of X } c= bool D

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { A where A is Subset of D : union A in the topology of X } or e in bool D )
assume e in { A where A is Subset of D : union A in the topology of X } ; :: thesis: e in bool D
then ex A being Subset of D st
( e = A & union A in the topology of X ) ;
hence e in bool D ; :: thesis: verum

end;

then reconsider t = { A where A is Subset of D : union A in the topology of X } as Subset-Family of D ;
set T = TopStruct(# D,t #);
TopStruct(# D,t #) is TopSpace-like

proof

union D = the carrier of X by EQREL_1:def 6;
then ( D c= D & union D in the topology of X ) by PRE_TOPC:def 1;
hence the carrier of TopStruct(# D,t #) in the topology of TopStruct(# D,t #) ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b₁ being Element of bool (bool the carrier of TopStruct(# D,t #)) holds
( not b₁ c= the topology of TopStruct(# D,t #) or union b₁ in the topology of TopStruct(# D,t #) ) ) & ( for b₁, b₂ being Element of bool the carrier of TopStruct(# D,t #) holds
( not b₁ in the topology of TopStruct(# D,t #) or not b₂ in the topology of TopStruct(# D,t #) or b₁ /\ b₂ in the topology of TopStruct(# D,t #) ) ) )
thus for a being Subset-Family of TopStruct(# D,t #) st a c= the topology of TopStruct(# D,t #) holds
union a in the topology of TopStruct(# D,t #) :: thesis: for b₁, b₂ being Element of bool the carrier of TopStruct(# D,t #) holds
( not b₁ in the topology of TopStruct(# D,t #) or not b₂ in the topology of TopStruct(# D,t #) or b₁ /\ b₂ in the topology of TopStruct(# D,t #) )

proof

let a be Subset-Family of TopStruct(# D,t #); :: thesis: ( a c= the topology of TopStruct(# D,t #) implies union a in the topology of TopStruct(# D,t #) )
A1: { (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= bool the carrier of X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } or e in bool the carrier of X )
assume e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } ; :: thesis: e in bool the carrier of X
then consider A being Subset of TopStruct(# D,t #) such that
A2: e = union A and
A in a ;
e c= the carrier of X

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in e or u in the carrier of X )
assume u in e ; :: thesis: u in the carrier of X
then consider x being set such that
A3: u in x and
A4: x in A by A2, TARSKI:def 4;
x in the carrier of TopStruct(# D,t #) by A4;
hence u in the carrier of X by A3; :: thesis: verum

end;

hence e in bool the carrier of X ; :: thesis: verum

end;

assume A5: a c= the topology of TopStruct(# D,t #) ; :: thesis: union a in the topology of TopStruct(# D,t #)
{ (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= the topology of X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } or e in the topology of X )
assume e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } ; :: thesis: e in the topology of X
then consider A being Subset of TopStruct(# D,t #) such that
A6: e = union A and
A7: A in a ;
A in the topology of TopStruct(# D,t #) by A5, A7;
then ex B being Subset of D st
( A = B & union B in the topology of X ) ;
hence e in the topology of X by A6; :: thesis: verum

end;

then union { (union A) where A is Subset of TopStruct(# D,t #) : A in a } in the topology of X by A1, PRE_TOPC:def 1;
then union (union a) in the topology of X by Th17;
hence union a in the topology of TopStruct(# D,t #) ; :: thesis: verum

end;

let a, b be Subset of TopStruct(# D,t #); :: thesis: ( not a in the topology of TopStruct(# D,t #) or not b in the topology of TopStruct(# D,t #) or a /\ b in the topology of TopStruct(# D,t #) )
assume that
A8: a in the topology of TopStruct(# D,t #) and
A9: b in the topology of TopStruct(# D,t #) ; :: thesis: a /\ b in the topology of TopStruct(# D,t #)
consider B being Subset of D such that
A10: b = B and
A11: union B in the topology of X by A9;
consider A being Subset of D such that
A12: a = A and
A13: union A in the topology of X by A8;
union (A /\ B) = (union A) /\ (union B) by Th26;
then union (A /\ B) in the topology of X by A13, A11, PRE_TOPC:def 1;
hence a /\ b in the topology of TopStruct(# D,t #) by A12, A10; :: thesis: verum

end;

then reconsider T = TopStruct(# D,t #) as strict TopSpace ;
take T ; :: thesis: ( the carrier of T = D & the topology of T = { A where A is Subset of D : union A in the topology of X } )
thus ( the carrier of T = D & the topology of T = { A where A is Subset of D : union A in the topology of X } ) ; :: thesis: verum