defpred S_{1}[ Element of FT] means U_FT $1 c= A;

{ 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 : U_FT x c= A } is Subset of FT ; :: thesis: verum

{ x where x is Element of FT : S

hence { x where x is Element of FT : U_FT x c= A } is Subset of FT ; :: thesis: verum