defpred S₁[ Element of FT] means U_FT $1 meets A;
{ x where x is Element of FT : S₁[x] } is Subset of FT from DOMAIN_1:sch 7();
hence { x where x is Element of FT : U_FT x meets A } is Subset of FT ; :: thesis: verum