defpred S1[ Element of ] means ex y being Element of st
( y in A & $1 in U_FT y );
{ x where x is Element of : S1[x] } is Subset of
from DOMAIN_1:sch 7();
hence
{ x where x is Element of : ex y being Element of st
( y in A & x in U_FT y ) } is Subset of
; verum