defpred S₁[ Element of T] means for y being Element of T st y in A ` holds
not $1 in U_FT y;
{ x where x is Element of T : S<sub>1</sub>[x] } is Subset of T from DOMAIN_1:sch 7();
hence { x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y } is Subset of T ; :: thesis: verum