let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
let A1 be SetSequence of X; :: thesis: lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf (A (\+\) A1) or x in A \+\ (lim_inf A1) )
assume x in lim_inf (A (\+\) A1) ; :: thesis: x in A \+\ (lim_inf A1)
then consider n1 being Element of NAT such that
A1: for k being Element of NAT holds x in (A (\+\) A1) . (n1 + k) by KURATO_2:7;

A2: now

let k be Element of NAT ; :: thesis: ( ( x in A & not x in A1 . (n1 + k) ) or ( not x in A & x in A1 . (n1 + k) ) )
x in (A (\+\) A1) . (n1 + k) by A1;
then x in A \+\ (A1 . (n1 + k)) by Def9;
hence ( ( x in A & not x in A1 . (n1 + k) ) or ( not x in A & x in A1 . (n1 + k) ) ) by XBOOLE_0:1; :: thesis: verum

end;

assume not x in A \+\ (lim_inf A1) ; :: thesis: contradiction
then A3: ( ( not x in A & not x in lim_inf A1 ) or ( x in lim_inf A1 & x in A ) ) by XBOOLE_0:1;

per cases ( ( not x in A & ( for n being Element of NAT holds
not for k being Element of NAT holds x in A1 . (n + k) ) ) or ( x in A & ex n being Element of NAT st
for k being Element of NAT holds x in A1 . (n + k) ) ) by A3, KURATO_2:7;

suppose A4: ( not x in A & ( for n being Element of NAT holds
not for k being Element of NAT holds x in A1 . (n + k) ) ) ; :: thesis: contradiction

then consider k1 being Element of NAT such that
A5: not x in A1 . (n1 + k1) ;
thus contradiction by A2, A4, A5; :: thesis: verum

end;

suppose A6: ( x in A & ex n being Element of NAT st
for k being Element of NAT holds x in A1 . (n + k) ) ; :: thesis: contradiction

then consider n2 being Element of NAT such that
A7: for k being Element of NAT holds x in A1 . (n2 + k) ;
x in A1 . (n2 + n1) by A7;
hence contradiction by A2, A6; :: thesis: verum

end;

end;