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 n being Element of NAT such that
A1: for k being Element of NAT holds x in (A (\) A1) . (n + k) by KURATO_2:7;

A2: now

let k be Element of NAT ; :: thesis: ( x in A & not x in A1 . (n + k) )
x in (A (\) A1) . (n + k) by A1;
then x in A \ (A1 . (n + k)) by Def7;
hence ( x in A & not x in A1 . (n + k) ) by XBOOLE_0:def 5; :: thesis: verum

end;

not x in lim_inf A1

proof

assume x in lim_inf A1 ; :: thesis: contradiction
then consider n1 being Element of NAT such that
A3: for k being Element of NAT holds x in A1 . (n1 + k) by KURATO_2:7;
x in A1 . (n1 + n) by A3;
hence contradiction by A2; :: thesis: verum

end;

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