defpred S₁[ Element of FMT] means ex V being Subset of FMT st
( V in U_FMT $1 & V c= A );
{ x where x is Element of FMT : S₁[x] } is Subset of FMT from DOMAIN_1:sch 7();
hence { x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } is Subset of FMT ; :: thesis: verum