let T be set ; :: thesis: for F being SetSequence of T st F is non-descending holds
lim_sup F = Union F
let F be SetSequence of T; :: thesis: ( F is non-descending implies lim_sup F = Union F )
assume A1: F is non-descending ; :: thesis: lim_sup F = Union F
thus lim_sup F c= Union F by Th8; :: according to XBOOLE_0:def 10 :: thesis: Union F c= lim_sup F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union F or x in lim_sup F )
assume x in Union F ; :: thesis: x in lim_sup F
then consider n being Nat such that
A2: x in F . n by PROB_1:12;
assume not x in lim_sup F ; :: thesis: contradiction
then consider m being Nat such that
A3: for k being Nat holds not x in F . (m + k) by Th5;
A4: not x in F . (m + 0) by A3;

per cases ( n <= m or n > m ) ;

suppose n <= m ; :: thesis: contradiction

then F . n c= F . m by A1, PROB_1:def 5;
hence contradiction by A2, A4; :: thesis: verum

end;

suppose n > m ; :: thesis: contradiction

then consider h being Nat such that
A5: n = m + h by NAT_1:10;
thus contradiction by A2, A3, A5; :: thesis: verum

end;

end;