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 object ; :: 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 Nat holds x in B . (0 + k) by PROB_1:13;
hence x in lim_inf B by KURATO_0:4; :: thesis: verum