theorem :: TOPS_2:33

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st M c= union F holds
M = union (F | M)