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