let i, i1 be natural number ; :: thesis: ( 1 <= i & 1 <= i1 -' i implies i1 -' i < i1 )
assume A1: ( 1 <= i & 1 <= i1 -' i ) ; :: thesis: i1 -' i < i1
then i1 - i = ((i1 -' i) + i) - i by Th61
.= i1 -' i ;
hence i1 -' i < i1 by A1, XREAL_1:233; :: thesis: verum