defpred S_{1}[ Element of FT] means ( U_FT $1 meets A & U_FT $1 meets 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 meets A & U_FT x meets 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 meets A & U_FT x meets A ` ) } is Subset of FT ; :: thesis: verum