let N be Hausdorff complete meet-continuous Lawson TopLattice; :: 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
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;
then reconsider y = x as Element of S ;
A2: for y being Element of S ex J being Basis of y st
for X being Subset of S st X in J holds
( X is open & X is filtered ) by WAYBEL14:35;
A3: ex_sup_of { (inf X) where X is Subset of S : ( y in X & X in sigma S ) } ,S by YELLOW_0:17;
InclPoset (sigma S) is continuous by WAYBEL14:36;
hence x = "\/" { (inf X) where X is Subset of S : ( y in X & X in sigma S ) } ,S by A2, WAYBEL14:37
.= "\/" { (inf X) where X is Subset of S : ( x in X & X in sigma S ) } ,N by A1, A3, YELLOW_0:26
.= "\/" { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N by Th34 ;
:: thesis: verum