theorem :: KURATO_2:28

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