set TS = TopStruct(# X,(UniCl D) #);
( the carrier of TopStruct(# X,(UniCl D) #) in the topology of TopStruct(# X,(UniCl D) #) & ( for a being Subset-Family of TopStruct(# X,(UniCl D) #) st a c= the topology of TopStruct(# X,(UniCl D) #) holds
union a in the topology of TopStruct(# X,(UniCl D) #) ) & ( for a, b being Subset of TopStruct(# X,(UniCl D) #) st a in the topology of TopStruct(# X,(UniCl D) #) & b in the topology of TopStruct(# X,(UniCl D) #) holds
a /\ b in the topology of TopStruct(# X,(UniCl D) #) ) ) by Th15, ROUGHS_4:def 3, FINSUB_1:def 2;
hence TopStruct(# X,(UniCl D) #) is TopSpace by PRE_TOPC:def 1; :: thesis: verum