let N be complete Lawson meet-continuous TopLattice; :: thesis: for S being Scott TopAugmentation of N

for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

let S be Scott TopAugmentation of N; :: thesis: for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

let x be Element of N; :: thesis: { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

set l = { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ;

set s = { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } ;

thus { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } c= { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } by Th33; :: according to XBOOLE_0:def 10 :: thesis: { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } c= { (inf A) where A is Subset of S : ( x in A & A in sigma S ) }

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } or k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } )

assume k in { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ; :: thesis: k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) }

then consider A being Subset of N such that

A1: k = inf A and

A2: x in A and

A3: A in lambda N ;

A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;

then reconsider J = A as Subset of S ;

A is open by A3, Th12;

then uparrow J is open by Th15;

then A5: uparrow J in sigma S by WAYBEL14:24;

A6: J c= uparrow J by WAYBEL_0:16;

inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27

.= inf (uparrow J) by WAYBEL_0:38, YELLOW_0:17 ;

hence k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } by A5, A1, A2, A6; :: thesis: verum

for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

let S be Scott TopAugmentation of N; :: thesis: for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

let x be Element of N; :: thesis: { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

set l = { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ;

set s = { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } ;

thus { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } c= { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } by Th33; :: according to XBOOLE_0:def 10 :: thesis: { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } c= { (inf A) where A is Subset of S : ( x in A & A in sigma S ) }

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } or k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } )

assume k in { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ; :: thesis: k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) }

then consider A being Subset of N such that

A1: k = inf A and

A2: x in A and

A3: A in lambda N ;

A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;

then reconsider J = A as Subset of S ;

A is open by A3, Th12;

then uparrow J is open by Th15;

then A5: uparrow J in sigma S by WAYBEL14:24;

A6: J c= uparrow J by WAYBEL_0:16;

inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27

.= inf (uparrow J) by WAYBEL_0:38, YELLOW_0:17 ;

hence k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } by A5, A1, A2, A6; :: thesis: verum