let T be TopSpace; :: thesis: {} T is open_condensed
Cl ({} T) = {} T by PRE_TOPC:22;
then Int (Cl ({} T)) = {} T ;
hence {} T is open_condensed by TOPS_1:def 8; :: thesis: verum