let X be set ; :: thesis: for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_inf A = B
let A be SetSequence of X; :: thesis: for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_inf A = B
let B be Subset of X; :: thesis: ( ( for n being Nat holds A . n = B ) implies lim_inf A = B )
assume A1: for n being Nat holds A . n = B ; :: thesis: lim_inf A = B
thus lim_inf A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= lim_inf A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf A or x in B )
assume x in lim_inf A ; :: thesis: x in B
then consider m being Nat such that
A2: for k being Nat holds x in A . (m + k) by Th4;
x in A . (m + 0) by A2;
hence x in B by A1; :: thesis: verum

end;

thus B c= lim_inf A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in lim_inf A )
assume A3: x in B ; :: thesis: x in lim_inf A
ex m being Nat st
for k being Nat holds x in A . (m + k)

proof

take 0 ; :: thesis: for k being Nat holds x in A . (0 + k)
let k be Nat; :: thesis: x in A . (0 + k)
thus x in A . (0 + k) by A1, A3; :: thesis: verum

end;

hence x in lim_inf A by Th4; :: thesis: verum

end;