let N be Scott TopLattice; :: thesis: for X being upper Subset of N holds Int X c= X ^0
let X be upper Subset of N; :: thesis: Int X c= X ^0
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int X or x in X ^0 )
assume A1: x in Int X ; :: thesis: x in X ^0
then reconsider y = x as Element of N ;
now :: thesis: for D being non empty directed Subset of N st y <= sup D holds
X meets D
A2: ( Int X is upper & Int X is inaccessible ) by WAYBEL11:def 4;
let D be non empty directed Subset of N; :: thesis: ( y <= sup D implies X meets D )
assume y <= sup D ; :: thesis: X meets D
then sup D in Int X by A2, A1;
then D meets Int X by A2;
hence X meets D by TOPS_1:16, XBOOLE_1:63; :: thesis: verum
end;
hence x in X ^0 ; :: thesis: verum