theorem :: XPRIMET1:88

for k being Nat
for p being Prime st p * p <= k & k < 38809 & 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 & not p = 61 & not p = 67 & not p = 71 & not p = 73 & not p = 79 & not p = 83 & not p = 89 & not p = 97 & not p = 101 & not p = 103 & not p = 107 & not p = 109 & not p = 113 & not p = 127 & not p = 131 & not p = 137 & not p = 139 & not p = 149 & not p = 151 & not p = 157 & not p = 163 & not p = 167 & not p = 173 & not p = 179 & not p = 181 & not p = 191 holds
p = 193