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