theorem Th16: :: CANTOR_1:16

for X being non empty set
for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #) by Def2, Th1, TOPS_2:64;