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:235
.= i + (j -' i) by A1, XREAL_1:235 ;
hence j -' (j -' i) = i ; :: thesis: verum