let X be set ; :: thesis: for F being SetSequence of X
for x being object holds
( x in lim_inf F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
let F be SetSequence of X; :: thesis: for x being object holds
( x in lim_inf F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
let x be object ; :: thesis: ( x in lim_inf F iff ex n being Nat st
for k being Nat holds x in F . (n + k) )
consider f being SetSequence of X such that
A1: lim_inf F = Union f and
A2: for n being Nat holds f . n = meet (F ^\ n) by Def1;

hereby :: thesis: ( ex n being Nat st
for k being Nat holds x in F . (n + k) implies x in lim_inf F )

consider f being SetSequence of X such that
A3: lim_inf F = Union f and
A4: for n being Nat holds f . n = meet (F ^\ n) by Def1;
assume x in lim_inf F ; :: thesis: ex n being Nat st
for k being Nat holds x in F . (n + k)
then consider n being Nat such that
A5: x in f . n by A3, PROB_1:12;
set G = F ^\ n;
reconsider n = n as Nat ;
take n = n; :: thesis: for k being Nat holds x in F . (n + k)
let k be Nat; :: thesis: x in F . (n + k)
A6: (F ^\ n) . k = F . (n + k) by NAT_1:def 3;
x in meet (F ^\ n) by A4, A5;
hence x in F . (n + k) by A6, Th3; :: thesis: verum

end;

given n being Nat such that A7: for k being Nat holds x in F . (n + k) ; :: thesis: x in lim_inf F
set G = F ^\ n;
for z being Nat holds x in (F ^\ n) . z

proof

let z be Nat; :: thesis: x in (F ^\ n) . z
(F ^\ n) . z = F . (n + z) by NAT_1:def 3;
hence x in (F ^\ n) . z by A7; :: thesis: verum

end;

then x in meet (F ^\ n) by Th3;
then x in f . n by A2;
hence x in lim_inf F by A1, PROB_1:12; :: thesis: verum