theorem Th16: :: TDLAT_1:16
for T being TopSpace
for A being Subset of T st A is condensed holds
A ` is condensed