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

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

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

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

end;

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

A5: ( not x <=' y -' z & not z <=' y -' x ) by A1, A2, A3, Lm8;
A6: x = y by A1, A4, Th4;
then x -' (x -' z) = z by A2, Lm6
.= z -' (x -' x) by Lm3, Lm4 ;
hence (y -' z) - x = [{} ,(z -' (y -' x))] by A5, A6, Def2
.= (y -' x) - z by A5, Def2 ;
:: thesis: verum

end;

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

A9: ( not x <=' y -' z & not z <=' y -' x ) by A1, A2, A7, Lm8;
A10: z = y by A2, A8, Th4;
x -' (z -' z) = x by Lm3, Lm4
.= z -' (z -' x) by A1, A10, Lm6 ;
hence (y -' z) - x = [{} ,(z -' (y -' x))] by A9, A10, Def2
.= (y -' x) - z by A9, Def2 ;
:: thesis: verum

end;

suppose that A11: not x + z <=' y and
A12: ( not y <=' x & not y <=' z ) ; :: thesis: (y -' z) - x = (y -' x) - z

A13: ( not x <=' y -' z & not z <=' y -' x ) by A1, A2, A11, Lm8;
x -' (y -' z) = z -' (y -' x) by A12, Lm13;
hence (y -' z) - x = [{} ,(z -' (y -' x))] by A13, Def2
.= (y -' x) - z by A13, Def2 ;
:: thesis: verum

end;

end;