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