let N be complete Lawson continuous TopLattice; :: thesis: ( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices )
thus ( N is compact & N is Hausdorff ) ; :: thesis: ( N is topological_semilattice & N is with_open_semilattices )
InclPoset (sigma N) is continuous ;
hence N is topological_semilattice by Th22; :: thesis: N is with_open_semilattices
thus N is with_open_semilattices ; :: thesis: verum