let T be TopSpace; :: thesis: [#] T is closed_condensed
Int ([#] T) = [#] T by TOPS_1:15;
then Cl (Int ([#] T)) = [#] T by TOPS_1:2;
hence [#] T is closed_condensed by TOPS_1:def 7; :: thesis: verum