set Q = { p where p is Element of P : len p <= n } ;
{ p where p is Element of P : len p <= n } c= P

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Element of P : len p <= n } or a in P )
assume a in { p where p is Element of P : len p <= n } ; :: thesis: a in P
then consider p being Element of P such that
A1: a = p and
len p <= n ;
thus a in P by A1; :: thesis: verum

end;

hence { p where p is Element of P : len p <= n } is Subset of P ; :: thesis: verum