defpred S₁[ Element of FT] means ( $1 in A & (U_FT $1) \ {$1} misses 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 : ( x in A & (U_FT x) \ {x} misses A ) } is Subset of FT ; :: thesis: verum