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

per cases ( z -' y <=' x or not z -' y <=' x ) ;

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

then A3: z <=' x + y by Lm7;
(x -' (z -' y)) + (z -' y) = x by A2, Def1
.= (x + z) -' z by Lm5
.= (x + (y + (z -' y))) -' z by A1, Def1
.= ((x + y) + (z -' y)) -' z by ARYTM_2:6
.= ((x + y) -' z) + (z -' y) by A3, Th13 ;
hence x -' (z -' y) = (x + y) -' z by ARYTM_2:11; :: thesis: verum

end;

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

then A5: not z <=' x + y by Lm7;
thus x -' (z -' y) = {} by A4, Def1
.= (x + y) -' z by A5, Def1 ; :: thesis: verum

end;

end;