defpred S₁[ Element of W] means len $1 = n;
{ w where w is Element of W : S₁[w] } is Subset of W from DOMAIN_1:sch 7();
hence { w where w is Element of W : len w = n } is Level of W by Def4; :: thesis: verum