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 consider k being Element of NAT such that
A2: for n being Element of NAT holds x in S . (k + n) by Th7;
reconsider p = x as Point of (Euclid 2) by A1, TOPREAL3:13;
reconsider y = x as Point of (TOP-REAL 2) by A1;
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 A3: 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
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 13;
then A5: x in S . m by A2, A4;
x in Ball p,r by A3, GOBOARD6:4;
hence S . m meets Ball p,r by A5, XBOOLE_0:3; :: thesis: verum

end;

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