defpred S₁[ Element of ] means ( $1 in A & ex V being Subset of st
( V in U_FMT $1 & V \ {$1} misses A ) );
{ x where x is Element of : S₁[x] } is Subset of from DOMAIN_1:sch 7();
hence { x where x is Element of : ( x in A & ex V being Subset of st
( V in U_FMT x & V \ {x} misses A ) ) } is Subset of ; :: thesis: verum