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
proof
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;
A8: Int X c= uparrow (Int X) by WAYBEL_0:16;
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