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 Element of NAT st
for k being Element of 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 Element of NAT st
for k being Element of NAT holds x in F . (n + k) )
let x be set ; :: thesis: ( x in Lim_K F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) )
Lim_K F = lim_inf F by Def9;
hence ( x in Lim_K F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) ) by Th7; :: thesis: verum