let X be set ; :: thesis: for F being convergent SetSequence of X
for x being set holds
( x in Lim_K F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
let F be convergent SetSequence of X; :: thesis: for x being set holds
( x in Lim_K F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
let x be set ; :: thesis: ( x in Lim_K F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
Lim_K F = lim_inf F by Def5;
hence ( x in Lim_K F iff ex n being Nat st
for k being Nat holds x in F . (n + k) ) by Th4; :: thesis: verum