for S being SetSequence of (TOP-REAL 2) holds lim_inf S c= Lim_inf S