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) )
assume A1: x in (lim_sup A1) \ (lim_sup A2) ; :: thesis: x in lim_sup (A1 (\) A2)
then not x in lim_sup A2 by XBOOLE_0:def 5;
then consider n1 being Nat such that
A2: for k being Nat holds not x in A2 . (n1 + k) by KURATO_0:5;
assume not x in lim_sup (A1 (\) A2) ; :: thesis: contradiction
then consider n2 being Nat such that
A3: for k being Nat holds not x in (A1 (\) A2) . (n2 + k) by KURATO_0:5;

A4: now :: thesis: for k being Nat holds
( not x in A1 . (n2 + k) or x in A2 . (n2 + k) )

let k be Nat; :: thesis: ( not x in A1 . (n2 + k) or x in A2 . (n2 + k) )
not x in (A1 (\) A2) . (n2 + k) by A3;
then not x in (A1 . (n2 + k)) \ (A2 . (n2 + k)) by Def3;
hence ( not x in A1 . (n2 + k) or x in A2 . (n2 + k) ) by XBOOLE_0:def 5; :: thesis: verum

end;

x in lim_sup A1 by A1, XBOOLE_0:def 5;
then consider k1 being Nat such that
A5: x in A1 . ((n1 + n2) + k1) by KURATO_0:5;
A6: x in A1 . (n2 + (k1 + n1)) by A5;
not x in A2 . (n1 + (n2 + k1)) by A2;
hence contradiction by A4, A6; :: thesis: verum