for S being Hausdorff compact TopLattice
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