defpred S₁[ Element of FMT] means for W being Subset of FMT st W in U_FMT $1 holds
W meets A;
{ x where x is Element of FMT : S₁[x] } is Subset of FMT from DOMAIN_1:sch 7();
hence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } is Subset of FMT ; :: thesis: verum