let m, n, x, y be Nat; :: thesis: ( x <= m & n = (m -' x) + y implies x -' (m -' n) = y -' (n -' m) )
assume Z0: x <= m ; :: thesis: ( not n = (m -' x) + y or x -' (m -' n) = y -' (n -' m) )
assume Z1: n = (m -' x) + y ; :: thesis: x -' (m -' n) = y -' (n -' m)
then ( m -' n <= x & n -' m <= y ) by Th5;
then A2: ( x -' (m -' n) = x - (m -' n) & y -' (n -' m) = y - (n -' m) ) by XREAL_1:233;
A3: n - y = m - x by Z0, Z1, XREAL_1:233;

per cases ( m <= n or m > n ) ;

suppose m <= n ; :: thesis: x -' (m -' n) = y -' (n -' m)

then A4: ( m -' n = 0 & n -' m = n - m ) by NAT_2:8, XREAL_1:233;
hence x -' (m -' n) = x by A2
.= (y - n) + m by A3
.= y -' (n -' m) by A2, A4 ;
:: thesis: verum

end;

suppose m > n ; :: thesis: x -' (m -' n) = y -' (n -' m)

then A5: ( n -' m = 0 & m -' n = m - n ) by NAT_2:8, XREAL_1:233;
hence x -' (m -' n) = (x - m) + n by A2
.= y by A3
.= y -' (n -' m) by A2, A5 ;
:: thesis: verum

end;

end;