let i be Nat; :: thesis: ( 1 < i implies 0 < i -' 1 )
assume 1 < i ; :: thesis: 0 < i -' 1
then ( 1 - 1 = 0 & 1 -' 1 < i -' 1 ) by NAT_D:56;
hence 0 < i -' 1 by XREAL_0:def 2; :: thesis: verum