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