let L be non empty Hausdorff compact TopSpace; :: thesis: for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) holds
for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N
let N be net of L; :: thesis: ( ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) implies for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N )
assume A1: for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ; :: thesis: for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N
let c be Point of L; :: thesis: ( c is_a_cluster_point_of N implies c in Lim N )
assume A2: c is_a_cluster_point_of N ; :: thesis: c in Lim N
assume not c in Lim N ; :: thesis: contradiction
then consider M being subnet of N such that
A3: for P being subnet of M holds not c in Lim P by YELLOW_6:37;
consider d being Point of L such that
A4: d is_a_cluster_point_of M by Th30;
A5: d is_a_cluster_point_of N by A4, Th31;
c <> d by A3, A4, Th32;
hence contradiction by A1, A2, A5; :: thesis: verum