let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\) A1) = A \ (lim_sup A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\) A1) = A \ (lim_sup A1)
let A1 be SetSequence of X; :: thesis: ( A1 is convergent implies lim_sup (A (\) A1) = A \ (lim_sup A1) )
assume A1: A1 is convergent ; :: thesis: lim_sup (A (\) A1) = A \ (lim_sup A1)
thus lim_sup (A (\) A1) c= A \ (lim_sup A1) :: according to XBOOLE_0:def 10 :: thesis: A \ (lim_sup A1) c= lim_sup (A (\) A1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup (A (\) A1) or x in A \ (lim_sup A1) )
assume A2: x in lim_sup (A (\) A1) ; :: thesis: x in A \ (lim_sup A1)
A3: for n being Nat ex k being Nat st
( x in A & not x in A1 . (n + k) )

proof

let n be Nat; :: thesis: ex k being Nat st
( x in A & not x in A1 . (n + k) )
consider k being Nat such that
A4: x in (A (\) A1) . (n + k) by A2, KURATO_0:5;
x in A \ (A1 . (n + k)) by A4, Def7;
then ( x in A & not x in A1 . (n + k) ) by XBOOLE_0:def 5;
hence ex k being Nat st
( x in A & not x in A1 . (n + k) ) ; :: thesis: verum

end;

A5: x in A

proof

A6: for n being Nat ex k being Nat st x in A

proof

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

end;

assume not x in A ; :: thesis: contradiction
then for n being Nat holds not x in A ;
hence contradiction by A6; :: thesis: verum

end;

for n being Nat holds
not for k being Nat holds x in A1 . (n + k)

proof

let n be Nat; :: thesis: not for k being Nat holds x in A1 . (n + k)
ex k being Nat st
( x in A & not x in A1 . (n + k) ) by A3;
hence not for k being Nat holds x in A1 . (n + k) ; :: thesis: verum

end;

then not x in lim_inf A1 by KURATO_0:4;
then not x in lim_sup A1 by A1, KURATO_0:def 5;
hence x in A \ (lim_sup A1) by A5, XBOOLE_0:def 5; :: thesis: verum

end;

thus A \ (lim_sup A1) c= lim_sup (A (\) A1) by Th83; :: thesis: verum