let T be non empty TopSpace; :: thesis: for N being net of T
for S being Subset of T st N is_eventually_in S holds
Lim N c= Cl S
let N be net of T; :: thesis: for S being Subset of T st N is_eventually_in S holds
Lim N c= Cl S
let S be Subset of T; :: thesis: ( N is_eventually_in S implies Lim N c= Cl S )
given i being Element of N such that A1: for j being Element of N st j >= i holds
N . j in S ; :: according to WAYBEL_0:def 11 :: thesis: Lim N c= Cl S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim N or x in Cl S )
assume A2: x in Lim N ; :: thesis: x in Cl S
then reconsider x = x as Element of T ;

now :: thesis: for G being a_neighborhood of x holds G meets S

let G be a_neighborhood of x; :: thesis: G meets S
N is_eventually_in G by A2, YELLOW_6:def 15;
then consider k being Element of N such that
A3: for j being Element of N st j >= k holds
N . j in G ;
[#] N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#] N and
A4: j >= i and
A5: j >= k ;
A6: N . j in G by A3, A5;
N . j in S by A1, A4;
hence G meets S by A6, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl S by CONNSP_2:27; :: thesis: verum