let N be complete 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 ) } c= { (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 ) } c= { (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 ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
set s = { (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 A) where A is Subset of S : ( x in A & A in sigma S ) } or k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } )
assume k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } ; :: thesis: k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
then consider J being Subset of S such that
A1: k = inf J and
A2: x in J and
A3: J in sigma S ;
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 A = J as Subset of N ;
sigma N c= lambda N by Th10;
then A5: sigma S c= lambda N by A4, YELLOW_9:52;
inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27;
hence k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } by A5, A1, A2, A3; :: thesis: verum