let N be Hausdorff complete Lawson meet-continuous 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)

set S = the complete Scott TopAugmentation of N;

A1: InclPoset (sigma the complete Scott TopAugmentation of N) is continuous by WAYBEL14:36;

A2: RelStr(# the carrier of the complete Scott TopAugmentation of N, the InternalRel of the complete Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

then reconsider y = x as Element of the complete Scott TopAugmentation of N ;

for y being Element of the complete Scott TopAugmentation of N ex J being Basis of y st

for X being Subset of the complete Scott TopAugmentation of N st X in J holds

( X is open & X is filtered ) by WAYBEL14:35;

hence x = "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( y in X & X in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A1, WAYBEL14:37

.= "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } ,N) by A2, YELLOW_0:17, YELLOW_0:26

.= "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by Th34 ;

:: thesis: verum

let x be Element of N; :: thesis: x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)

set S = the complete Scott TopAugmentation of N;

A1: InclPoset (sigma the complete Scott TopAugmentation of N) is continuous by WAYBEL14:36;

A2: RelStr(# the carrier of the complete Scott TopAugmentation of N, the InternalRel of the complete Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;

then reconsider y = x as Element of the complete Scott TopAugmentation of N ;

for y being Element of the complete Scott TopAugmentation of N ex J being Basis of y st

for X being Subset of the complete Scott TopAugmentation of N st X in J holds

( X is open & X is filtered ) by WAYBEL14:35;

hence x = "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( y in X & X in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A1, WAYBEL14:37

.= "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } ,N) by A2, YELLOW_0:17, YELLOW_0:26

.= "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by Th34 ;

:: thesis: verum