for N being Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice holds N is with_compact_semilattices