defpred S₁[ Element of ] means for D being non empty directed Subset of st $1 <= sup D holds
X meets D;
thus { u where u is Element of : S₁[u] } is Subset of from DOMAIN_1:sch 7(); :: thesis: verum