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