let N be complete Lawson meet-continuous TopLattice; :: thesis: for S being Scott TopAugmentation of N

for X being upper Subset of N

for Y being Subset of S st X = Y holds

Int X = Int Y

let S be Scott TopAugmentation of N; :: thesis: for X being upper Subset of N

for Y being Subset of S st X = Y holds

Int X = Int Y

let X be upper Subset of N; :: thesis: for Y being Subset of S st X = Y holds

Int X = Int Y

let Y be Subset of S; :: thesis: ( X = Y implies Int X = Int Y )

assume A1: X = Y ; :: thesis: Int X = Int 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 K = uparrow (Int X) as Subset of S ;

reconsider sX = Int X as Subset of S by A2;

A3: K c= Y

uparrow sX is open by Th15;

then K is open by A2, WAYBEL_0:13;

then uparrow (Int X) c= Int Y by A3, TOPS_1:24;

hence Int X c= Int Y by A8; :: according to XBOOLE_0:def 10 :: thesis: Int Y c= Int X

reconsider A = Int Y as Subset of N by A2;

N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def 4;

then A is open by WAYBEL19:37;

hence Int Y c= Int X by A1, TOPS_1:16, TOPS_1:24; :: thesis: verum

for X being upper Subset of N

for Y being Subset of S st X = Y holds

Int X = Int Y

let S be Scott TopAugmentation of N; :: thesis: for X being upper Subset of N

for Y being Subset of S st X = Y holds

Int X = Int Y

let X be upper Subset of N; :: thesis: for Y being Subset of S st X = Y holds

Int X = Int Y

let Y be Subset of S; :: thesis: ( X = Y implies Int X = Int Y )

assume A1: X = Y ; :: thesis: Int X = Int 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 K = uparrow (Int X) as Subset of S ;

reconsider sX = Int X as Subset of S by A2;

A3: K c= Y

proof

A8:
Int X c= uparrow (Int X)
by WAYBEL_0:16;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in K or a in Y )

A4: Int X c= X by TOPS_1:16;

assume A5: a in K ; :: thesis: a in Y

then reconsider x = a as Element of N ;

A6: X c= uparrow X by WAYBEL_0:16;

uparrow X c= X by WAYBEL_0:24;

then A7: uparrow X = X by A6;

ex y being Element of N st

( y <= x & y in Int X ) by A5, WAYBEL_0:def 16;

hence a in Y by A7, A1, A4, WAYBEL_0:def 16; :: thesis: verum

end;A4: Int X c= X by TOPS_1:16;

assume A5: a in K ; :: thesis: a in Y

then reconsider x = a as Element of N ;

A6: X c= uparrow X by WAYBEL_0:16;

uparrow X c= X by WAYBEL_0:24;

then A7: uparrow X = X by A6;

ex y being Element of N st

( y <= x & y in Int X ) by A5, WAYBEL_0:def 16;

hence a in Y by A7, A1, A4, WAYBEL_0:def 16; :: thesis: verum

uparrow sX is open by Th15;

then K is open by A2, WAYBEL_0:13;

then uparrow (Int X) c= Int Y by A3, TOPS_1:24;

hence Int X c= Int Y by A8; :: according to XBOOLE_0:def 10 :: thesis: Int Y c= Int X

reconsider A = Int Y as Subset of N by A2;

N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def 4;

then A is open by WAYBEL19:37;

hence Int Y c= Int X by A1, TOPS_1:16, TOPS_1:24; :: thesis: verum