let X be set ; :: thesis: for F being SetSequence of X holds meet F c= lim_inf F
let F be SetSequence of X; :: thesis: meet F c= lim_inf F
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet F or x in lim_inf F )
assume x in meet F ; :: thesis: x in lim_inf F
then for k being Element of NAT holds x in F . (0 + k) by Th6;
hence x in lim_inf F by Th7; :: thesis: verum