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 set ; :: 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 Element of NAT such that
A1: for k being Element of NAT holds x in F . (n + k) by Th7;

now

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

end;

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