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