let p be odd Prime; :: thesis: p + 1 > 3
p + 1 > 2 + 1 by lem3, XREAL_1:8;
hence p + 1 > 3 ; :: thesis: verum