let b be Nat; :: thesis: ( b > 1 implies |.(1 / b).| < 1 )
assume b > 1 ; :: thesis: |.(1 / b).| < 1
then 1 / b < 1 / 1 by XREAL_1:76;
hence |.(1 / b).| < 1 ; :: thesis: verum