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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup (A1 (\) A2) or x in (lim_sup A1) \ (lim_sup A2) )
assume A2: x in lim_sup (A1 (\) A2) ; :: thesis: x in (lim_sup A1) \ (lim_sup A2)

A3: now :: thesis: for n being Nat ex k being Nat st
( x in A1 . (n + k) & not x in A2 . (n + k) )

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

end;

assume not x in (lim_sup A1) \ (lim_sup A2) ; :: thesis: contradiction
then A5: ( not x in lim_sup A1 or x in lim_sup A2 ) by XBOOLE_0:def 5;

per cases ( not x in lim_sup A1 or x in lim_inf A2 ) by A1, A5, KURATO_0:def 5;

suppose not x in lim_sup A1 ; :: thesis: contradiction

then consider n1 being Nat such that
A6: for k being Nat holds not x in A1 . (n1 + k) by KURATO_0:5;
ex k2 being Nat st
( x in A1 . (n1 + k2) & not x in A2 . (n1 + k2) ) by A3;
hence contradiction by A6; :: thesis: verum

end;

suppose x in lim_inf A2 ; :: thesis: contradiction

then consider n2 being Nat such that
A7: for k being Nat holds x in A2 . (n2 + k) by KURATO_0:4;
ex k3 being Nat st
( x in A1 . (n2 + k3) & not x in A2 . (n2 + k3) ) by A3;
hence contradiction by A7; :: thesis: verum

end;

end;

end;

thus (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2) by Th69; :: thesis: verum