thus 1,2,3,4 are_mutually_distinct ; :: thesis: for n being positive Nat holds not 1 + n,2 + n,3 + n,4 + n are_mutually_coprime
given n being positive Nat such that A1: 1 + n,2 + n,3 + n,4 + n are_mutually_coprime ; :: thesis: contradiction

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: contradiction

hence contradiction by A1, NEWTON05:35, POLYFORM:6; :: thesis: verum

end;

suppose n is even ; :: thesis: contradiction

hence contradiction by A1, NEWTON05:35, POLYFORM:7; :: thesis: verum

end;

end;