let x, y, z be Element of REAL+ ; ( y <=' x & y <=' z implies x + (z -' y) = (x -' y) + z )
assume that
A1:
y <=' x
and
A2:
y <=' z
; x + (z -' y) = (x -' y) + z
(x + (z -' y)) + y =
x + ((z -' y) + y)
by ARYTM_2:6
.=
x + z
by A2, Def1
.=
((x -' y) + y) + z
by A1, Def1
.=
((x -' y) + z) + y
by ARYTM_2:6
;
hence
x + (z -' y) = (x -' y) + z
by ARYTM_2:11; verum