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 object ; :: 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 Nat such that
A1: for k being Nat holds x in (A (\+\) A1) . (n1 + k) by KURATO_0:4;

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

let k be 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 Nat holds
not for k being Nat holds x in A1 . (n + k) ) ) or ( x in A & ex n being Nat st
for k being Nat holds x in A1 . (n + k) ) ) by A3, KURATO_0:4;

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

then not for k1 being Nat holds x in A1 . (n1 + k1) ;
hence contradiction by A2, A4; :: thesis: verum

end;

suppose A5: ( x in A & ex n being Nat st
for k being Nat holds x in A1 . (n + k) ) ; :: thesis: contradiction

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

end;

end;