let X be set ; :: thesis: for F being SetSequence of X holds lim_sup F c= Union F
let F be SetSequence of X; :: thesis: lim_sup F c= Union F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup F or x in Union F )
assume x in lim_sup F ; :: thesis: x in Union F
then ex k being Nat st x in F . (0 + k) by Th5;
hence x in Union F by PROB_1:12; :: thesis: verum