let N be complete Lawson meet-continuous 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:1; :: thesis: verum