let S be SetSequence of (TOP-REAL 2); :: thesis: lim_inf S c= Lim_inf S
let x be set ; :: 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 Element of NAT such that
A2: for n being Element of NAT holds x in S . (k + n) by A1, KURATO_0:4;
for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p,r)

proof

let r be real number ; :: thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p,r) )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p,r)
then A3: x in Ball (p,r) by GOBOARD6:1;
take k ; :: thesis: for m being Element of NAT st m > k holds
S . m meets Ball (p,r)
let m be Element of 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;
h in NAT by ORDINAL1:def 12;
then 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 Th48;
hence x in Lim_inf S ; :: thesis: verum