let i, i1 be natural Number ; :: thesis: ( 1 <= i & 1 <= i1 -' i implies i1 -' i < i1 )
assume that
A1: 1 <= i and
A2: 1 <= i1 -' i ; :: thesis: i1 -' i < i1
i1 - i = ((i1 -' i) + i) - i by A2, Th43
.= i1 -' i ;
hence i1 -' i < i1 by A1, XREAL_1:231; :: thesis: verum