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