let T be non empty TopSpace; :: thesis:
let N be net of T; :: thesis:
let S be Subset of T; :: thesis:
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:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in Lim N ; :: thesis:
then reconsider x = x as Element of T ;

let G be a_neighborhood of x; :: thesis:
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:

end;