defpred S_{1}[ 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_{1}[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

( W meets A & W meets A ` );

{ x where x is Element of FMT : S

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