let a be Real; :: thesis: ( 1 < a implies (1 / a) - 1 < 0 )
assume 1 < a ; :: thesis: (1 / a) - 1 < 0
then 1 / a < 1 / 1 by XREAL_1:76;
then (1 / a) - 1 < 1 - 1 by XREAL_1:9;
hence (1 / a) - 1 < 0 ; :: thesis: verum