let a be Real; :: thesis: ( 1 <= a implies a -' 1 < a )
assume 1 <= a ; :: thesis: a -' 1 < a
then a -' 1 = a - 1 by Th233;
hence a -' 1 < a by Th44; :: thesis: verum