let S be Hausdorff compact TopLattice; :: thesis: for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N
let c be Point of S; :: thesis: for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N
let N be net of S; :: thesis: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N implies c = sup N )
assume A1: ( ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N ) ; :: thesis: c = sup N
reconsider c9 = c as Element of S ;
( c9 is_>=_than rng the mapping of N & ( for b being Element of S st rng the mapping of N is_<=_than b holds
c9 <= b ) ) by A1, Lm5, Lm6;
hence c = sup (rng the mapping of N) by YELLOW_0:30
.= sup N by YELLOW_2:def 5 ;
:: thesis: verum