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 set ; :: 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

A2: ( Int X is upper & Int X is inaccessible_by_directed_joins ) 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, WAYBEL_0:def 20;
then D meets Int X by A2, WAYBEL11:def 1;
hence X meets D by TOPS_1:16, XBOOLE_1:63; :: thesis: verum

end;

hence x in X ^0 ; :: thesis: verum