let S be SetSequence of (TOP-REAL 2); :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in lim_inf S ; :: thesis:
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:
assume r > 0 ; :: thesis:
then A3: x in Ball (p,r) by GOBOARD6:1;
reconsider k = k as Nat ;
take k ; :: thesis:
let m be Nat; :: thesis:
assume m > k ; :: thesis:
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:

end;

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