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

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

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

end;

assume A7: for n being Nat ex k being Nat st x in F . (n + k) ; :: thesis: x in lim_sup F
for z being Nat holds x in f . z

proof

let z be Nat; :: thesis: x in f . z
set G = F ^\ z;
consider k being Nat such that
A8: x in F . (z + k) by A7;
( f . z = Union (F ^\ z) & (F ^\ z) . k = F . (z + k) ) by A2, NAT_1:def 3;
hence x in f . z by A8, PROB_1:12; :: thesis: verum

end;

hence x in lim_sup F by A1, Th3; :: thesis: verum