let x, y, z be Element of REAL+ ; ( x <=' y & z <=' y implies (y -' z) - x = (y -' x) - z )
assume that
A1:
x <=' y
and
A2:
z <=' y
; (y -' z) - x = (y -' x) - z
per cases
( x + z <=' y or ( not x + z <=' y & y <=' x ) or ( not x + z <=' y & y <=' z ) or ( not x + z <=' y & not y <=' x & not y <=' z ) )
;
suppose that A5:
not
x + z <=' y
and A6:
y <=' x
;
(y -' z) - x = (y -' x) - zA7:
not
x <=' y -' z
by A2, A5, Lm8;
A8:
not
z <=' y -' x
by A1, A5, Lm8;
A9:
x = y
by A1, A6, Th4;
then x -' (x -' z) =
z
by A2, Lm6
.=
z -' (x -' x)
by Lm3, Lm4
;
hence (y -' z) - x =
[{},(z -' (y -' x))]
by A7, A9, Def2
.=
(y -' x) - z
by A8, Def2
;
verum end; suppose that A10:
not
x + z <=' y
and A11:
y <=' z
;
(y -' z) - x = (y -' x) - zA12:
not
x <=' y -' z
by A2, A10, Lm8;
A13:
not
z <=' y -' x
by A1, A10, Lm8;
A14:
z = y
by A2, A11, Th4;
x -' (z -' z) =
x
by Lm3, Lm4
.=
z -' (z -' x)
by A1, A14, Lm6
;
hence (y -' z) - x =
[{},(z -' (y -' x))]
by A12, A14, Def2
.=
(y -' x) - z
by A13, Def2
;
verum end; end;