let S be SetSequence of (TOP-REAL 2); :: thesis: lim_inf S c= Lim_inf S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf S or x in Lim_inf S )
assume A1: x in lim_inf S ; :: thesis: x in Lim_inf S
then reconsider p = x as Point of (Euclid 2) by TOPREAL3:8;
reconsider y = x as Point of (TOP-REAL 2) by A1;
consider k being Nat such that
A2: for n being Nat holds x in S . (k + n) by A1, KURATO_0:4;
for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p,r)

proof

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p,r) )
assume r > 0 ; :: thesis: ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p,r)
then A3: x in Ball (p,r) by GOBOARD6:1;
reconsider k = k as Nat ;
take k ; :: thesis: for m being Nat st m > k holds
S . m meets Ball (p,r)
let m be Nat; :: thesis: ( m > k implies S . m meets Ball (p,r) )
assume m > k ; :: thesis: S . m meets Ball (p,r)
then consider h being Nat such that
A4: m = k + h by NAT_1:10;
x in S . m by A2, A4;
hence S . m meets Ball (p,r) by A3, XBOOLE_0:3; :: thesis: verum

end;

then y in Lim_inf S by Th14;
hence x in Lim_inf S ; :: thesis: verum