let p be Prime; :: thesis: ( p is odd implies 9 <= p ^2 )
assume p is odd ; :: thesis: 9 <= p ^2
then 3 <= p by Lm3;
then 3 * 3 <= p * p by XREAL_1:66;
hence 9 <= p ^2 ; :: thesis: verum