theorem Th30: :: WAYBEL_9:30

for T being non empty Hausdorff compact TopSpace
for N being net of T ex c being Point of T st c is_a_cluster_point_of N