let p be Prime; :: thesis: ( p > 2 implies not p + 1 is Prime )
assume S1: p > 2 ; :: thesis: p + 1 is not Prime
then p + 1 > 2 + 1 by XREAL_1:8;
then S3: p + 1 > 2 by XXREAL_0:2;
p is odd by S1, PEPIN:17;
hence p + 1 is not Prime by S3, PEPIN:17; :: thesis: verum