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