let N be complete Lawson continuous TopLattice; :: thesis: ( N is compact & N is T_2 & N is topological_semilattice & N is with_open_semilattices )
thus ( N is compact & N is T_2 ) ; :: 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