for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N )