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