let i, j be natural number ; :: thesis: ( i <= j implies j -' (j -' i) = i )
assume A1: i <= j ; :: thesis: j -' (j -' i) = i
(j -' (j -' i)) + (j -' i) = j by Th50, XREAL_1:237
.= i + (j -' i) by A1, XREAL_1:237 ;
hence j -' (j -' i) = i ; :: thesis: verum