let N be complete meet-continuous Lawson TopLattice; :: thesis: ( N is continuous iff for x being Element of N holds x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N )
consider S being complete 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: ( ( for x being Element of N holds x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N ) implies N is continuous )

assume A2: N is continuous ; :: thesis: for x being Element of N holds x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N
let x be Element of N; :: thesis: x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N
A3: S is continuous by A2;
then A4: InclPoset (sigma S) is continuous by WAYBEL14:36;
A5: ex_sup_of { (inf X) where X is Subset of S : ( x in X & X in sigma S ) } ,N by YELLOW_0:17;
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 ) by A3, WAYBEL14:35;
hence x = "\/" { (inf X) where X is Subset of S : ( x in X & X in sigma S ) } ,S by A1, A4, WAYBEL14:37
.= "\/" { (inf X) where X is Subset of S : ( x in X & X in sigma S ) } ,N by A1, A5, YELLOW_0:26
.= "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N by Th34 ;
:: thesis: verum

end;

assume A6: for x being Element of N holds x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N ; :: thesis: N is continuous

now

let x be Element of S; :: thesis: x = "\/" { (inf V) where V is Subset of S : ( x in V & V in sigma S ) } ,S
A7: ex_sup_of { (inf X) where X is Subset of S : ( x in X & X in sigma S ) } ,N by YELLOW_0:17;
thus x = "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N by A1, A6
.= "\/" { (inf V) where V is Subset of S : ( x in V & V in sigma S ) } ,N by A1, Th34
.= "\/" { (inf V) where V is Subset of S : ( x in V & V in sigma S ) } ,S by A1, A7, YELLOW_0:26 ; :: thesis: verum

end;

then S is continuous by WAYBEL14:38;
hence N is continuous by A1, YELLOW12:15; :: thesis: verum