:: deftheorem defines ^0 WAYBEL30:def 1 :
for N being non empty reflexive RelStr
for X being Subset of N holds X ^0 = { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D } ;