let T be TopSpace; :: thesis: {} T is condensed
( Int ({} T) c= {} T & {} T c= Cl ({} T) ) by PRE_TOPC:48;
then ( Int (Cl ({} T)) c= {} T & {} T c= Cl (Int ({} T)) ) by PRE_TOPC:52;
hence {} T is condensed by TOPS_1:def 6; :: thesis: verum