let i, i1, i2 be natural Number ; :: thesis: ( i >= i1 implies i >= i1 -' i2 )
assume A1: i >= i1 ; :: thesis: i >= i1 -' i2
i1 >= i1 -' i2 by Th35;
hence i >= i1 -' i2 by A1, XXREAL_0:2; :: thesis: verum