let S be Hausdorff compact TopLattice; :: thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous )
assume A1: for x being Element of S holds x "/\" is continuous ; :: thesis: S is meet-continuous
then for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) by Th38;
hence S is meet-continuous by A1, Th37; :: thesis: verum