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 set ; :: 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: now

let n be Element of NAT ; :: thesis: ex k being Element of NAT st
( ( x in A & not x in A1 . (n + k) ) or ( not x in A & x in A1 . (n + k) ) )
consider k1 being Element of NAT such that
A4: x in (A (\+\) A1) . (n + k1) by A2, KURATO_2:8;
x in A \+\ (A1 . (n + k1)) by A4, Def9;
then ( ( x in A & not x in A1 . (n + k1) ) or ( not x in A & x in A1 . (n + k1) ) ) by XBOOLE_0:1;
hence ex k being Element of NAT st
( ( x in A & not x in A1 . (n + k) ) or ( not x in A & x in A1 . (n + k) ) ) ; :: thesis: verum

end;

assume A5: not x in A \+\ (lim_sup A1) ; :: thesis: contradiction

per cases ( ( not x in A & not x in lim_sup A1 ) or ( x in A & x in lim_sup A1 ) ) by A5, XBOOLE_0:1;

suppose A6: ( not x in A & not x in lim_sup A1 ) ; :: thesis: contradiction

then consider n1 being Element of NAT such that
A7: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_2:8;
ex k1 being Element of NAT st
( ( x in A & not x in A1 . (n1 + k1) ) or ( not x in A & x in A1 . (n1 + k1) ) ) by A3;
hence contradiction by A6, A7; :: thesis: verum

end;

suppose A8: ( x in A & x in lim_sup A1 ) ; :: thesis: contradiction

then x in lim_inf A1 by A1, KURATO_2:def 7;
then consider n2 being Element of NAT such that
A9: for k being Element of NAT holds x in A1 . (n2 + k) by KURATO_2:7;
ex k2 being Element of NAT st
( ( x in A & not x in A1 . (n2 + k2) ) or ( not x in A & x in A1 . (n2 + k2) ) ) by A3;
hence contradiction by A8, A9; :: thesis: verum

end;

end;

end;

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