let X be set ; :: thesis:
let F be SetSequence of X; :: thesis:
let x be object ; :: thesis:
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;

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:
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:
let k be Nat; :: thesis:
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:

end;

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

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

end;