let N be complete meet-continuous Lawson 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;
A3: Int X c= uparrow (Int X) by WAYBEL_0:16;
reconsider sX = Int X as Subset of S by A2;
reconsider K = uparrow (Int X) as Subset of S by A2;
uparrow sX is open by Th15;
then A4: K is open by A2, WAYBEL_0:13;
K c= Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in K or a in Y )
assume A5: a in K ; :: thesis: a in Y
then reconsider x = a as Element of N ;
consider y being Element of N such that
A6: ( y <= x & y in Int X ) by A5, WAYBEL_0:def 16;
A7: Int X c= X by TOPS_1:44;
uparrow X = X

proof

thus uparrow X c= X by WAYBEL_0:24; :: according to XBOOLE_0:def 10 :: thesis: X c= uparrow X
thus X c= uparrow X by WAYBEL_0:16; :: thesis: verum

end;

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

end;

then uparrow (Int X) c= Int Y by A4, TOPS_1:56;
hence Int X c= Int Y by A3, XBOOLE_1:1; :: 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:44, TOPS_1:56; :: thesis: verum