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

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

assume N is continuous ; :: thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous )
then A3: S is continuous ;
for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S

proof

let x be Point of S; :: thesis: ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S
consider J being Basis of x such that
A4: for W being Subset of S st W in J holds
( W is open & W is filtered ) by A3, WAYBEL14:35;
take J ; :: thesis: for W being Subset of S st W in J holds
W is Filter of S
let W be Subset of S; :: thesis: ( W in J implies W is Filter of S )
assume A5: W in J ; :: thesis: W is Filter of S
then W is open by A4;
hence W is Filter of S by A4, A5, WAYBEL11:def 4, YELLOW_8:21; :: thesis: verum

end;

hence N is with_open_semilattices by Th32; :: thesis: InclPoset (sigma N) is continuous
InclPoset (sigma S) is continuous by A3, WAYBEL14:36;
hence InclPoset (sigma N) is continuous by A1, YELLOW_9:52; :: thesis: verum

end;

assume A6: ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) ; :: thesis: N is continuous
for x being Element of S ex J being Basis of x st
for Y being Subset of S st Y in J holds
( Y is open & Y is filtered )

proof

let x be Element of S; :: thesis: ex J being Basis of x st
for Y being Subset of S st Y in J holds
( Y is open & Y is filtered )
reconsider y = x as Element of N by A1;
consider J being Basis of y such that
A7: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A6, Def4;
reconsider J' = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;
take J' ; :: thesis: for Y being Subset of S st Y in J' holds
( Y is open & Y is filtered )
let Y be Subset of S; :: thesis: ( Y in J' implies ( Y is open & Y is filtered ) )
assume A8: Y in J' ; :: thesis: ( Y is open & Y is filtered )
then consider A being Subset of N such that
A9: Y = uparrow A and
A10: A in J ;
subrelstr A is meet-inheriting by A7, A10;
then A is filtered by YELLOW12:26;
then uparrow A is filtered ;
hence ( Y is open & Y is filtered ) by A1, A8, A9, WAYBEL_0:4, YELLOW_8:21; :: thesis: verum

end;

then for x being Element of S holds x = "\/" { (inf X) where X is Subset of S : ( x in X & X in sigma S ) } ,S by A2, A6, WAYBEL14:37;
then S is continuous by WAYBEL14:38;
hence N is continuous by A1, YELLOW12:15; :: thesis: verum