X ^0 = {}

proof

thus X ^0 c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= X ^0

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X ^0 or a in {} )
assume that
A1: a in X ^0 and
not a in {} ; :: thesis: contradiction
consider u being Element of N such that
A2: ( a = u & ( for D being non empty directed Subset of N st u <= sup D holds
X meets D ) ) by A1;
reconsider D = {u} as non empty directed Subset of N by WAYBEL_0:5;
A3: u <= sup D by YELLOW_0:39;
X misses D by XBOOLE_1:65;
hence contradiction by A2, A3; :: thesis: verum

end;

thus {} c= X ^0 by XBOOLE_1:2; :: thesis: verum

end;

hence X ^0 is empty ; :: thesis: verum