let x, y, z be Element of REAL+ ; :: thesis: ( not z <=' y implies x - (z -' y) = (x + y) - z )
assume A1: not z <=' y ; :: 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 z <=' x + y by Lm7;
then A3: (x + y) - z = (x + y) -' z by Def2;
x - (z -' y) = x -' (z -' y) by A2, Def2;
hence x - (z -' y) = (x + y) - z by A1, A3, Lm11; :: thesis: verum

end;

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

then A5: not z <=' x + y by Lm7;
(z -' y) -' x = z -' (x + y) by Lm9;
hence x - (z -' y) = [{},(z -' (x + y))] by A4, Def2
.= (x + y) - z by A5, Def2 ;
:: thesis: verum

end;

end;