X ^0 c= {}

proof

let a be object ; :: 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
a = u and
A2: 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: X misses D ;
u <= sup D by YELLOW_0:39;
hence contradiction by A3, A2; :: thesis: verum

end;

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