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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_sup A1) \ (lim_sup A2) or x in lim_sup (A1 (\) A2) )
assume x in (lim_sup A1) \ (lim_sup A2) ; :: thesis: x in lim_sup (A1 (\) A2)
then A1: ( x in lim_sup A1 & not x in lim_sup A2 ) by XBOOLE_0:def 5;
then consider n1 being Element of NAT such that
A2: for k being Element of NAT holds not x in A2 . (n1 + k) by KURATO_2:8;
assume not x in lim_sup (A1 (\) A2) ; :: thesis: contradiction
then consider n2 being Element of NAT such that
A3: for k being Element of NAT holds not x in (A1 (\) A2) . (n2 + k) by KURATO_2:8;

A4: now

let k be Element of 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;

consider k1 being Element of NAT such that
A5: x in A1 . ((n1 + n2) + k1) by A1, KURATO_2:8;
( x in A1 . ((n1 + n2) + k1) & not x in A2 . (n1 + (n2 + k1)) ) by A2, A5;
then ( x in A1 . (n2 + (k1 + n1)) & not x in A2 . (n2 + (k1 + n1)) ) ;
hence contradiction by A4; :: thesis: verum