let X be set ; :: thesis: for F being SetSequence of X
for x being set holds
( x in lim_inf F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) )
let F be SetSequence of X; :: thesis: for x being set holds
( x in lim_inf F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) )
let x be set ; :: thesis: ( x in lim_inf F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) )

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

assume A1: x in lim_inf F ; :: thesis: ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k)
consider f being SetSequence of X such that
A2: ( lim_inf F = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) by Def3;
consider n being Element of NAT such that
A3: x in f . n by A1, A2, PROB_1:25;
take n = n; :: thesis: for k being Element of NAT holds x in F . (n + k)
let k be Element of NAT ; :: thesis: x in F . (n + k)
A4: x in meet (F ^\ n) by A2, A3;
set G = F ^\ n;
(F ^\ n) . k = F . (n + k) by NAT_1:def 3;
hence x in F . (n + k) by A4, Th6; :: thesis: verum

end;

given n being Element of NAT such that A5: for k being Element of NAT holds x in F . (n + k) ; :: thesis: x in lim_inf F
set G = F ^\ n;
consider f being SetSequence of X such that
A6: ( lim_inf F = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) by Def3;
for z being Element of NAT holds x in (F ^\ n) . z

proof

let z be Element of 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 A5; :: thesis: verum

end;

then x in meet (F ^\ n) by Th6;
then x in f . n by A6;
hence x in lim_inf F by A6, PROB_1:25; :: thesis: verum