theorem
for
k being
Nat for
p being
Prime st
p * p <= k &
k < 4489 & not
p = 2 & not
p = 3 & not
p = 5 & not
p = 7 & not
p = 11 & not
p = 13 & not
p = 17 & not
p = 19 & not
p = 23 & not
p = 29 & not
p = 31 & not
p = 37 & not
p = 41 & not
p = 43 & not
p = 47 & not
p = 53 & not
p = 59 holds
p = 61