theorem Th3: :: FINTOPO7:4

for X being non empty set
for B being Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
( UniCl B = UniCl (FinMeetCl B) & TopStruct(# X,(UniCl B) #) is TopSpace-like )