defpred S_{1}[ Element of FMT] means ( $1 in A & ex V being Subset of FMT st

( V in U_FMT $1 & V \ {$1} misses 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 : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT ; :: thesis: verum

( V in U_FMT $1 & V \ {$1} misses A ) );

{ x where x is Element of FMT : S

hence { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st

( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT ; :: thesis: verum