theorem
for
k being
Nat for
p being
Prime st
p * p <= k &
k < 2809 & 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 holds
p = 47