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 set ; :: 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 consider k being Element of NAT such that
A1: x in F . (0 + k) by Th8;
thus x in Union F by A1, PROB_1:25; :: thesis: verum