let T be non empty TopSpace; :: thesis: for S being SetSequence of the carrier of T holds Lim_inf S is closed
let S be SetSequence of the carrier of T; :: thesis: Lim_inf S is closed
Lim_inf S = Cl (Lim_inf S) by Th51;
hence Lim_inf S is closed ; :: thesis: verum