defpred S_{1}[ 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_{1}[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

( y in A & $1 in U_FT y );

{ x where x is Element of FT : S

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