let L be non empty TopSpace; :: thesis: for N being net of L
for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
let N be net of L; :: thesis: for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
let M be subnet of N; :: thesis: for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
let c be Point of L; :: thesis: ( c is_a_cluster_point_of M implies c is_a_cluster_point_of N )
assume A1: c is_a_cluster_point_of M ; :: 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
M is_often_in O by A1, Def9;
hence N is_often_in O by YELLOW_6:27; :: thesis: verum