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