let i be Element of NAT ; :: thesis: ( 1 < i implies 0 < i -' 1 )
assume A1: 1 < i ; :: thesis: 0 < i -' 1
A2: 1 - 1 = 0 ;
1 -' 1 < i -' 1 by A1, NAT_D:56;
hence 0 < i -' 1 by A2, XREAL_0:def 2; :: thesis: verum