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

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