let a be real number ; :: thesis: ( 1 <= a implies a -' 1 < a )
assume 1 <= a ; :: thesis: a -' 1 < a
then a -' 1 = a - 1 by Th235;
hence a -' 1 < a by Th46; :: thesis: verum