let L be non empty TopSpace; :: thesis: for N being net of L
for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N
let N be net of L; :: thesis: for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N
let c be Point of L; :: thesis: ( c in Lim N implies c is_a_cluster_point_of N )
assume A1: c in Lim N ; :: thesis: c is_a_cluster_point_of N
let O be a_neighborhood of c; :: according to WAYBEL_9:def 9 :: thesis: N is_often_in O
N is_eventually_in O by A1, YELLOW_6:def 15;
hence N is_often_in O by YELLOW_6:19; :: thesis: verum