theorem Th36: :: WAYBEL_9:36

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-filtered & c is_a_cluster_point_of N holds
c = inf N