let p be Prime; :: thesis: ( p > 2 implies ReciProducts (p + 1) = ReciProducts p )
assume p > 2 ; :: thesis: ReciProducts (p + 1) = ReciProducts p
then not p + 1 is prime by P1NotPrime;
then SetPrimes (p + 1) = SetPrimes p by PrimesSet;
hence ReciProducts (p + 1) = ReciProducts p ; :: thesis: verum