for X being non empty set
for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)