let p be Prime; :: thesis: ( p is odd implies 3 <= p )
1 < p by INT_2:def 4;
then 1 + 1 <= p by NAT_1:13;
then ( 2 = p or 2 < p ) by XXREAL_0:1;
then ( 2 = p or 2 + 1 <= p ) by NAT_1:13;
hence ( p is odd implies 3 <= p ) ; :: thesis: verum