for k being Nat st k < 841 holds
for n being Nat st n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds
n = 23 by Lm6;