let x, y, z be Element of REAL+ ; :: thesis: (z -' y) -' x = z -' (x + y)

per cases ( x + y <=' z or x = {} or ( not y <=' z & x <> {} ) or ( not x + y <=' z & y <=' z ) ) ;

suppose A1: x + y <=' z ; :: thesis: (z -' y) -' x = z -' (x + y)

y <=' x + y by ARYTM_2:19;
then A2: y <=' z by A1, Th3;
then A3: x <=' z -' y by A1, Lm8;
((z -' y) -' x) + (x + y) = (((z -' y) -' x) + x) + y by ARYTM_2:6
.= (z -' y) + y by A3, Def1
.= z by A2, Def1 ;
hence (z -' y) -' x = z -' (x + y) by A1, Def1; :: thesis: verum

end;

suppose A4: x = {} ; :: thesis: (z -' y) -' x = z -' (x + y)

hence (z -' y) -' x = z -' y by Lm4
.= z -' (x + y) by A4, ARYTM_2:def 8 ;
:: thesis: verum

end;

suppose that A5: not y <=' z and
A6: x <> {} ; :: thesis: (z -' y) -' x = z -' (x + y)

y <=' y + x by ARYTM_2:19;
then A7: not x + y <=' z by A5, Th3;

now :: thesis: not x <=' z -' y

assume A8: x <=' z -' y ; :: thesis: contradiction
z -' y = {} by A5, Def1;
hence contradiction by A6, A8, Th5; :: thesis: verum

end;

hence (z -' y) -' x = {} by Def1
.= z -' (x + y) by A7, Def1 ;
:: thesis: verum

end;

suppose that A9: not x + y <=' z and
A10: y <=' z ; :: thesis: (z -' y) -' x = z -' (x + y)

not x <=' z -' y by A9, A10, Lm8;
hence (z -' y) -' x = {} by Def1
.= z -' (x + y) by A9, Def1 ;
:: thesis: verum

end;

end;