let p be odd Prime; :: thesis: p > 2
p > 1 by INT_2:def 4;
then p >= 1 + 1 by INT_1:7;
hence p > 2 by POLYFORM:5, XXREAL_0:1; :: thesis: verum