for T being TopSpace
for A being Subset of T st A is open holds
A is subcondensed by TOPS_1:23;