let n be non zero Nat; :: thesis: support (ppf n) c= Seg n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg n )
assume x in support (ppf n) ; :: thesis: x in Seg n
then A1: x in support (pfexp n) by NAT_3:def 9;
then reconsider k = x as Prime by NAT_3:34;
A3: 1 < k by INT_2:def 4;
k <= n by NAT_D:7, A1, NAT_3:36;
hence x in Seg n by FINSEQ_1:1, A3; :: thesis: verum