defpred S₁[ 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₁[u] } is Subset of N from DOMAIN_1:sch 7(); :: thesis: verum