let k be Nat; :: thesis: ( k < 25 implies for n being Nat st n * n <= k & n is prime & not n = 2 holds
n = 3 )
assume A1: k < 25 ; :: thesis: for n being Nat st n * n <= k & n is prime & not n = 2 holds
n = 3
let n be Nat; :: thesis: ( n * n <= k & n is prime & not n = 2 implies n = 3 )
assume that
A3: n * n <= k and
A4: n is prime ; :: thesis: ( n = 2 or n = 3 )
n * n < 5 * 5 by A1, A3, XXREAL_0:2;
then n < 5 by Th1;
hence ( n = 2 or n = 3 ) by A4, Lm2; :: thesis: verum