let T be TopSpace; :: thesis: [#] T is condensed
[#] T c= Cl ([#] T) by PRE_TOPC:18;
then A1: [#] T c= Cl (Int ([#] T)) by TOPS_1:15;
Int (Cl ([#] T)) c= [#] T ;
hence [#] T is condensed by A1, TOPS_1:def 6; :: thesis: verum