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

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

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

then z <=' x -' y by A1, Lm8;
then A3: (x -' y) - z = (x -' y) -' z by Def2;
x - (y + z) = x -' (y + z) by A2, Def2;
hence x - (y + z) = (x -' y) - z by A3, Lm9; :: thesis: verum

end;

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

A6: not z <=' x -' y by A1, A4, Lm8;
A7: (x + z) -' x = z by Lm5
.= z -' (x -' x) by Lm3, Lm4 ;
x = y by A1, A5, Th4;
hence x - (y + z) = [{},(z -' (x -' y))] by A4, A7, Def2
.= (x -' y) - z by A6, Def2 ;
:: thesis: verum

end;

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

A10: not z <=' x -' y by A1, A8, Lm8;
(y + z) -' x = z -' (x -' y) by A9, Lm11;
hence x - (y + z) = [{},(z -' (x -' y))] by A8, Def2
.= (x -' y) - z by A10, Def2 ;
:: thesis: verum

end;

end;