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