Lim_inf S = Cl (Lim_inf S) by Th15;
hence Lim_inf S is closed ; :: thesis: verum