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

let n be Nat; :: thesis:
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:

end;

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:

end;

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:

end;