theorem :: NEWTON02:200

for a, b, c being Nat holds
( not (a |^ 3) + (b |^ 3) = c |^ 3 or 7 divides a or 7 divides b or 7 divides c )