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