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

set S = the complete Scott TopAugmentation of N;

A1: 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;

hence N is continuous by A1, YELLOW12:15; :: thesis: verum

set S = the complete Scott TopAugmentation of N;

A1: 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;

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 A4:
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 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)

then A3: for x being Element of the complete Scott TopAugmentation of N ex J being Basis of x st

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

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

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

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

hence x = "\/" ( { (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 ) } , the complete Scott TopAugmentation of N) by A3, 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 A1, 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

end;then A3: for x being Element of the complete Scott TopAugmentation of N ex J being Basis of x st

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

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

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

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

hence x = "\/" ( { (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 ) } , the complete Scott TopAugmentation of N) by A3, 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 A1, 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

now :: thesis: for x being Element of the complete Scott TopAugmentation of N holds x = "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N)

then
the complete Scott TopAugmentation of N is continuous
by WAYBEL14:38;let x be Element of the complete Scott TopAugmentation of N; :: thesis: x = "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N)

thus x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by A1, A4

.= "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } ,N) by A1, Th34

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

end;thus x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by A1, A4

.= "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } ,N) by A1, Th34

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

hence N is continuous by A1, YELLOW12:15; :: thesis: verum