let k be Nat; :: thesis: for n being non zero Nat st support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k holds
k + 1 is Prime
let n be non zero Nat; :: thesis: ( support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k implies k + 1 is Prime )
assume that
A1: support (ppf n) c= Seg (k + 1) and
A2: not support (ppf n) c= Seg k ; :: thesis: k + 1 is Prime
k + 1 in support (ppf n)

proof

assume not k + 1 in support (ppf n) ; :: thesis: contradiction
then A3: {(k + 1)} misses support (ppf n) by ZFMISC_1:50;
(support (ppf n)) \ {(k + 1)} c= (Seg (k + 1)) \ {(k + 1)} by A1, XBOOLE_1:33;
then support (ppf n) c= (Seg (k + 1)) \ {(k + 1)} by A3, XBOOLE_1:83;
hence contradiction by A2, FINSEQ_1:10; :: thesis: verum

end;

then k + 1 in support (pfexp n) by NAT_3:def 9;
hence k + 1 is Prime by NAT_3:34; :: thesis: verum