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