let X be set ; :: thesis: for A1, A2 being SetSequence of X holds lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2)
let A1, A2 be SetSequence of X; :: thesis: lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf (A1 (\) A2) or x in (lim_inf A1) \ (lim_inf A2) )
assume x in lim_inf (A1 (\) A2) ; :: thesis: x in (lim_inf A1) \ (lim_inf A2)
then consider n being Nat such that
A1: for k being Nat holds x in (A1 (\) A2) . (n + k) by KURATO_0:4;

A2: now :: thesis: for k being Nat holds
( x in A1 . (n + k) & not x in A2 . (n + k) )

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

end;

A3: not x in lim_inf A2

proof

assume x in lim_inf A2 ; :: thesis: contradiction
then consider n1 being Nat such that
A4: for k being Nat holds x in A2 . (n1 + k) by KURATO_0:4;
x in A2 . (n1 + n) by A4;
hence contradiction by A2; :: thesis: verum

end;

x in lim_inf A1 by A2, KURATO_0:4;
hence x in (lim_inf A1) \ (lim_inf A2) by A3, XBOOLE_0:def 5; :: thesis: verum