for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A ) )