let N be complete meet-continuous Lawson TopLattice; :: thesis: ( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )
consider S being Scott TopAugmentation of N;
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of N,the InternalRel of N #) by YELLOW_9:def 4;

hereby :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic implies N is algebraic )

assume A2: N is algebraic ; :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic )
then reconsider M = N as algebraic LATTICE ;
M is continuous ;
hence N is with_open_semilattices ; :: thesis: InclPoset (sigma N) is algebraic
S is algebraic by A1, A2, WAYBEL_8:17;
then ex K being Basis of S st K = { (uparrow x) where x is Element of S : x in the carrier of (CompactSublatt S) } by WAYBEL14:42;
then InclPoset (sigma S) is algebraic by WAYBEL14:43;
hence InclPoset (sigma N) is algebraic by A1, YELLOW_9:52; :: thesis: verum

end;

assume that
A3: N is with_open_semilattices and
A4: InclPoset (sigma N) is algebraic ; :: thesis: N is algebraic
reconsider T = InclPoset (sigma N) as algebraic LATTICE by A4;
T is continuous ;
then N is continuous by A3, Th35;
then S is continuous ;
then for x being Element of S ex K being Basis of x st
for Y being Subset of S st Y in K holds
( Y is open & Y is filtered ) by WAYBEL14:35;
then A5: for V being Element of (InclPoset (sigma S)) ex VV being Subset of (InclPoset (sigma S)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma S)) st W in VV holds
W is co-prime ) ) by WAYBEL14:39;
InclPoset (sigma S) is algebraic by A1, A4, YELLOW_9:52;
then ex K being Basis of S st K = { (uparrow x) where x is Element of S : x in the carrier of (CompactSublatt S) } by A5, WAYBEL14:44;
then S is algebraic by WAYBEL14:45;
hence N is algebraic by A1, WAYBEL_8:17; :: thesis: verum