let T be non empty TopSpace; :: thesis: for N being net of T
for p being Point of T st p in Lim N holds
for d being Element of N ex S being Subset of T st
( S = { (N . c) where c is Element of N : d <= c } & p in Cl S )
let N be net of T; :: thesis: for p being Point of T st p in Lim N holds
for d being Element of N ex S being Subset of T st
( S = { (N . c) where c is Element of N : d <= c } & p in Cl S )
let p be Point of T; :: thesis: ( p in Lim N implies for d being Element of N ex S being Subset of T st
( S = { (N . c) where c is Element of N : d <= c } & p in Cl S ) )
assume A1: p in Lim N ; :: thesis: for d being Element of N ex S being Subset of T st
( S = { (N . c) where c is Element of N : d <= c } & p in Cl S )
let d be Element of N; :: thesis: ex S being Subset of T st
( S = { (N . c) where c is Element of N : d <= c } & p in Cl S )
{ (N . c) where c is Element of N : d <= c } c= the carrier of T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (N . c) where c is Element of N : d <= c } or x in the carrier of T )
assume x in { (N . c) where c is Element of N : d <= c } ; :: thesis: x in the carrier of T
then ex c being Element of N st
( x = N . c & d <= c ) ;
hence x in the carrier of T ; :: thesis: verum
end;
then reconsider S = { (N . c) where c is Element of N : d <= c } as Subset of T ;
take S ; :: thesis: ( S = { (N . c) where c is Element of N : d <= c } & p in Cl S )
thus S = { (N . c) where c is Element of N : d <= c } ; :: thesis: p in Cl S
now :: thesis: for G being a_neighborhood of p holds G meets S
let G be a_neighborhood of p; :: thesis: G meets S
N is_eventually_in G by A1, Def15;
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds
N . j in G ;
consider e being Element of N such that
A3: d <= e and
A4: i <= e by Def3;
A5: N . e in S by A3;
N . e in G by A2, A4;
hence G meets S by A5, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl S by CONNSP_2:27; :: thesis: verum