theorem :: NAT_4:60

for k being Nat st k < 25 holds
for n being Nat st n * n <= k & n is prime & not n = 2 holds
n = 3 by Lm3;