let N be complete meet-continuous Lawson TopLattice; :: thesis: for S being Scott TopAugmentation of N
for X being lower Subset of N
for Y being Subset of S st X = Y holds
Cl X = Cl Y
let S be Scott TopAugmentation of N; :: thesis: for X being lower Subset of N
for Y being Subset of S st X = Y holds
Cl X = Cl Y
let X be lower Subset of N; :: thesis: for Y being Subset of S st X = Y holds
Cl X = Cl Y
let Y be Subset of S; :: thesis: ( X = Y implies Cl X = Cl Y )
assume A1: X = Y ; :: thesis: Cl X = Cl Y
A2: 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 = Cl Y as Subset of N ;
(Cl X) ` = (Cl ((X ` ) ` )) `
.= Int (X ` ) by TOPS_1:def 1
.= Int (Y ` ) by A1, A2, Th17
.= (Cl ((Y ` ) ` )) ` by TOPS_1:def 1
.= A ` by A2 ;
hence Cl X = Cl Y by TOPS_1:21; :: thesis: verum