X ^0 c= {}

proof

hence
X ^0 is empty
; :: thesis: verum
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;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