theorem Th3: :: WAYBEL18:3

for X being set
for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like