theorem Th22: :: PRE_TOPC:22

for T being TopStruct
for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )