let n be Nat; :: thesis: ( n <> 0 implies (n + 1) / n > 1 )
assume A1: n <> 0 ; :: thesis: (n + 1) / n > 1
(n + 1) / n = (n / n) + (1 / n) by XCMPLX_1:62
.= 1 + (1 / n) by A1, XCMPLX_1:60 ;
hence (n + 1) / n > 1 by A1, XREAL_1:29; :: thesis: verum