theorem Th5: :: FRECHET:5
for T being TopStruct st {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds
meet F is closed ) holds
T is TopSpace