let k, n be Nat; :: thesis: ( k < 961 & 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 & not n = 23 implies n = 29 )

assume A1: k < 961 ; :: thesis: ( not n * n <= k or not n is prime or n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29 )

assume that

A2: n * n <= k and

A3: n is prime ; :: thesis: ( n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29 )

n * n < 31 * 31 by A1, A2, XXREAL_0:2;

hence ( n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29 ) by A3, Th11, NAT_4:1; :: thesis: verum

assume A1: k < 961 ; :: thesis: ( not n * n <= k or not n is prime or n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29 )

assume that

A2: n * n <= k and

A3: n is prime ; :: thesis: ( n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29 )

n * n < 31 * 31 by A1, A2, XXREAL_0:2;

hence ( n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29 ) by A3, Th11, NAT_4:1; :: thesis: verum