defpred S_{1}[ Element of N] means for D being non empty directed Subset of N st $1 <= sup D holds

X meets D;

thus { u where u is Element of N : S_{1}[u] } is Subset of N
from DOMAIN_1:sch 7(); :: thesis: verum

X meets D;

thus { u where u is Element of N : S