let T be non empty TopSpace; :: thesis: for P being Subset of T
for s being SetSequence of the carrier of T st ( for i being Nat holds s . i c= P ) holds
Lim_inf s c= Cl P
let P be Subset of T; :: thesis: for s being SetSequence of the carrier of T st ( for i being Nat holds s . i c= P ) holds
Lim_inf s c= Cl P
let s be SetSequence of the carrier of T; :: thesis: ( ( for i being Nat holds s . i c= P ) implies Lim_inf s c= Cl P )
assume A1: for i being Nat holds s . i c= P ; :: thesis: Lim_inf s c= Cl P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_inf s or x in Cl P )
assume A2: x in Lim_inf s ; :: thesis: x in Cl P
then reconsider p = x as Point of T ;
for G being Subset of T st G is open & p in G holds
P meets G
proof
let G be Subset of T; :: thesis: ( G is open & p in G implies P meets G )
assume A3: G is open ; :: thesis: ( not p in G or P meets G )
assume p in G ; :: thesis: P meets G
then reconsider G9 = G as a_neighborhood of p by A3, CONNSP_2:3;
consider k being Nat such that
A4: for m being Nat st m > k holds
s . m meets G9 by A2, Def1;
set m = k + 1;
k + 1 > k by NAT_1:13;
then s . (k + 1) meets G9 by A4;
hence P meets G by A1, XBOOLE_1:63; :: thesis: verum
end;
hence x in Cl P by PRE_TOPC:def 7; :: thesis: verum