{ i where i is Element of NAT : i < len p } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : i < len p } or x in NAT )
assume x in { i where i is Element of NAT : i < len p } ; :: thesis: x in NAT
then ex i being Element of NAT st
( i = x & i < len p ) ;
hence x in NAT ; :: thesis: verum

end;

hence proj1 p is Subset of NAT by AXIOMS:4; :: thesis: verum