let X be set ; :: thesis: for F being SetSequence of X holds lim_inf F c= lim_sup F
let F be SetSequence of X; :: thesis: lim_inf F c= lim_sup F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf F or x in lim_sup F )
assume x in lim_inf F ; :: thesis: x in lim_sup F
then consider n being Nat such that
A1: for k being Nat holds x in F . (n + k) by Th4;

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

let k be Nat; :: thesis: ex n being Nat st x in F . (k + n)
x in F . (n + k) by A1;
hence ex n being Nat st x in F . (k + n) ; :: thesis: verum

end;

hence x in lim_sup F by Th5; :: thesis: verum