let X be set ; :: thesis: for B being SetSequence of X holds Intersection B c= lim_inf B
let B be SetSequence of X; :: thesis: Intersection B c= lim_inf B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection B or x in lim_inf B )
assume x in Intersection B ; :: thesis: x in lim_inf B
then for k being Element of NAT holds x in B . (0 + k) by PROB_1:29;
hence x in lim_inf B by KURATO_2:7; :: thesis: verum