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

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