theorem Th31: :: WAYBEL_9:31

for L being non empty TopSpace
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 by YELLOW_6:18;