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

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

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

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

end;

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

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

end;

end;