let X be set ; :: thesis: for A1, A2 being SetSequence of X st A2 is convergent holds
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)
let A1, A2 be SetSequence of X; :: thesis: ( A2 is convergent implies lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2) )
assume A1: A2 is convergent ; :: thesis: lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)
thus lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2) by Th62; :: according to XBOOLE_0:def 10 :: thesis: (lim_inf A1) \ (lim_inf A2) c= lim_inf (A1 (\) A2)
thus (lim_inf A1) \ (lim_inf A2) c= lim_inf (A1 (\) A2) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_inf A1) \ (lim_inf A2) or x in lim_inf (A1 (\) A2) )
assume A2: x in (lim_inf A1) \ (lim_inf A2) ; :: thesis: x in lim_inf (A1 (\) A2)
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;

now :: thesis: for k being Nat holds x in (A1 (\) A2) . ((n0 + n1) + k)

let k be Nat; :: thesis: x in (A1 (\) A2) . ((n0 + n1) + k)
( 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: verum

end;

hence x in lim_inf (A1 (\) A2) by KURATO_0:4; :: thesis: verum

end;