let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in (lim_inf A1) \ (lim_inf A2) ; :: thesis:
then x in lim_inf A1 by XBOOLE_0:def 5;
then consider n0 being Nat such that
A3: for k being Nat holds x in A1 . (n0 + k) by KURATO_0:4;
not x in lim_inf A2 by A2, XBOOLE_0:def 5;
then not x in lim_sup A2 by A1, KURATO_0:def 5;
then consider n1 being Nat such that
A4: for k being Nat holds not x in A2 . (n1 + k) by KURATO_0:5;

let k be Nat; :: thesis:
( x in A1 . (n0 + (n1 + k)) & not x in A2 . (n1 + (n0 + k)) ) by A3, A4;
then x in (A1 . ((n0 + n1) + k)) \ (A2 . ((n0 + n1) + k)) by XBOOLE_0:def 5;
hence x in (A1 (\) A2) . ((n0 + n1) + k) by Def3; :: thesis:

end;

end;