let X be set ; :: thesis: for A1, A2 being SetSequence of X holds (lim_sup A1) \+\ (lim_sup A2) c= lim_sup (A1 (\+\) A2)
let A1, A2 be SetSequence of X; :: thesis: (lim_sup A1) \+\ (lim_sup A2) c= lim_sup (A1 (\+\) A2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_sup A1) \+\ (lim_sup A2) or x in lim_sup (A1 (\+\) A2) )
A1: for A1, A2 being SetSequence of X st x in lim_sup A1 & not x in lim_sup A2 holds
x in lim_sup (A1 (\+\) A2)

proof

let A1, A2 be SetSequence of X; :: thesis: ( x in lim_sup A1 & not x in lim_sup A2 implies x in lim_sup (A1 (\+\) A2) )
assume that
A2: x in lim_sup A1 and
A3: not x in lim_sup A2 ; :: thesis: x in lim_sup (A1 (\+\) A2)
consider n1 being Nat such that
A4: for k being Nat holds not x in A2 . (n1 + k) by A3, KURATO_0:5;

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

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

end;

hence x in lim_sup (A1 (\+\) A2) by KURATO_0:5; :: thesis: verum

end;

assume A6: x in (lim_sup A1) \+\ (lim_sup A2) ; :: thesis: x in lim_sup (A1 (\+\) A2)

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

suppose ( x in lim_sup A1 & not x in lim_sup A2 ) ; :: thesis: x in lim_sup (A1 (\+\) A2)

hence x in lim_sup (A1 (\+\) A2) by A1; :: thesis: verum

end;

suppose ( not x in lim_sup A1 & x in lim_sup A2 ) ; :: thesis: x in lim_sup (A1 (\+\) A2)

hence x in lim_sup (A1 (\+\) A2) by A1; :: thesis: verum

end;

end;