let n be Nat; :: thesis: ( n <> 0 implies (n + 1) / n > 1 )
assume A1: n <> 0 ; :: thesis: (n + 1) / n > 1
then A2: n > 0 ;
A3: (n + 1) / n = (n / n) + (1 / n) by XCMPLX_1:63
.= 1 + (1 / n) by A1, XCMPLX_1:60 ;
1 / n > 0 by A2;
hence (n + 1) / n > 1 by A3, XREAL_1:31; :: thesis: verum