defpred S₁[ Subset of ] means alphaInt $1 = sInt $1;
{ B where B is Subset of : S₁[B] } is Subset-Family of from DOMAIN_1:sch 7();
hence { B where B is Subset of : alphaInt B = sInt B } is Subset-Family of ; :: thesis: verum