let T be non empty TopSpace; :: thesis: for F being SetSequence of the carrier of T
for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A
let F be SetSequence of the carrier of T; :: thesis: for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A
let A be closed Subset of T; :: thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = A )
assume for i being Nat holds F . i = A ; :: thesis: Lim_inf F = A
then Lim_inf F = Cl A by Th23;
hence Lim_inf F = A by PRE_TOPC:22; :: thesis: verum