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