let T be TopSpace; :: thesis: {} T is closed_condensed
Cl (Int ({} T)) = {} T by PRE_TOPC:22;
hence {} T is closed_condensed by TOPS_1:def 7; :: thesis: verum