let N be complete meet-continuous Lawson 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 ) }
A1: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of S,the InternalRel of S #) by YELLOW_9:def 4;
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 set ; :: 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
A2: ( k = inf A & x in A & A in lambda N ) ;
reconsider J = A as Subset of S by A1;
A3: ex_inf_of J,S by YELLOW_0:17;
then A4: inf A = inf J by A1, YELLOW_0:27
.= inf (uparrow J) by A3, WAYBEL_0:38 ;
A5: J c= uparrow J by WAYBEL_0:16;
A is open by A2, Th12;
then uparrow J is open by Th15;
then uparrow J in sigma S by WAYBEL14:24;
hence k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } by A2, A4, A5; :: thesis: verum