defpred S1[ Element of ] means for W being Subset of st W in U_FMT $1 holds
( W meets A & W meets A ` );
{ x where x is Element of : S1[x] } is Subset of
from DOMAIN_1:sch 7();
hence
{ x where x is Element of : for W being Subset of st W in U_FMT x holds
( W meets A & W meets A ` ) } is Subset of
; verum