let k be Nat; :: thesis: for p being Prime st p * p <= k & k < 25 & not p = 2 holds
p = 3
let p be Prime; :: thesis: ( p * p <= k & k < 25 & not p = 2 implies p = 3 )
assume ( p * p <= k & k < 25 ) ; :: thesis: ( p = 2 or p = 3 )
then p * p < 5 * 5 by XXREAL_0:2;
hence ( p = 2 or p = 3 ) by Ttool5a, NAT_4:1; :: thesis: verum