assume ex n being Nat st
( n is perfect_power & n + 1 is perfect_power & n + 2 is perfect_power & n + 3 is perfect_power ) ; :: thesis: contradiction
then consider n being Nat such that
A1: ( n is perfect_power & n + 1 is perfect_power & n + 2 is perfect_power & n + 3 is perfect_power ) ;
consider k being Nat such that
A3: ( n = 4 * k or n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) by NUMBER02:24;

per cases ( n = 4 * k or n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) by A3;

suppose n = 4 * k ; :: thesis: contradiction

hence contradiction by A1, Four2NotPerfect; :: thesis: verum

end;

suppose n = (4 * k) + 1 ; :: thesis: contradiction

then n + 1 = (4 * k) + 2 ;
hence contradiction by A1, Four2NotPerfect; :: thesis: verum

end;

suppose n = (4 * k) + 2 ; :: thesis: contradiction

hence contradiction by A1, Four2NotPerfect; :: thesis: verum

end;

suppose n = (4 * k) + 3 ; :: thesis: contradiction

then n + 3 = (4 * (k + 1)) + 2 ;
hence contradiction by A1, Four2NotPerfect; :: thesis: verum

end;

end;