let n be Nat; :: thesis: 1 < n + 2
( 0 < n + 1 implies 1 < n + 2 )

proof

assume 0 < n + 1 ; :: thesis: 1 < n + 2
0 + 1 = 1 ;
hence 1 < n + 2 by XREAL_1:8; :: thesis: verum

end;

hence 1 < n + 2 ; :: thesis: verum