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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ (lim_inf A1) or x in lim_inf (A (\) A1) )
assume A2: x in A \ (lim_inf A1) ; :: thesis: x in lim_inf (A (\) A1)
then x in A \ (lim_sup A1) by A1, KURATO_2:def 7;
then not x in lim_sup A1 by XBOOLE_0:def 5;
then consider n1 being Element of NAT such that
A3: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_2:8;
assume A4: not x in lim_inf (A (\) A1) ; :: thesis: contradiction
A5: for n being Element of NAT holds
( not x in A or ex k being Element of NAT st x in A1 . (n + k) )

proof

let n be Element of NAT ; :: thesis: ( not x in A or ex k being Element of NAT st x in A1 . (n + k) )
consider k being Element of NAT such that
A6: not x in (A (\) A1) . (n + k) by A4, KURATO_2:7;
not x in A \ (A1 . (n + k)) by A6, Def7;
then ( not x in A or x in A1 . (n + k) ) by XBOOLE_0:def 5;
hence ( not x in A or ex k being Element of NAT st x in A1 . (n + k) ) ; :: thesis: verum

end;

per cases ( not x in A or ex k being Element of NAT st x in A1 . (n1 + k) ) by A5;

suppose not x in A ; :: thesis: contradiction

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

suppose ex k being Element of NAT st x in A1 . (n1 + k) ; :: thesis: contradiction

then consider k being Element of NAT such that
A7: x in A1 . (n1 + k) ;
thus contradiction by A3, A7; :: thesis: verum

end;

end;

end;