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 A3: x + z <=' y ; :: thesis: (y -' z) - x = (y -' x) - z
then z <=' y -' x by A1, Lm8;
then A4: (y -' x) -' z = (y -' x) - z by Def2;
x <=' y -' z by A2, A3, Lm8;
then (y -' z) -' x = (y -' z) - x by Def2;
hence (y -' z) - x = (y -' x) - z by A4, Lm10; :: thesis: verum
end;
suppose that A5: not x + z <=' y and
A6: y <=' x ; :: thesis: (y -' z) - x = (y -' x) - z
A7: not x <=' y -' z by A2, A5, Lm8;
A8: not z <=' y -' x by A1, A5, Lm8;
A9: x = y by A1, A6, Th4;
then x -' (x -' z) = z by A2, Lm6
.= z -' (x -' x) by Lm3, Lm4 ;
hence (y -' z) - x = [{},(z -' (y -' x))] by A7, A9, Def2
.= (y -' x) - z by A8, Def2 ;
:: thesis: verum
end;
suppose that A10: not x + z <=' y and
A11: y <=' z ; :: thesis: (y -' z) - x = (y -' x) - z
A12: not x <=' y -' z by A2, A10, Lm8;
A13: not z <=' y -' x by A1, A10, Lm8;
A14: z = y by A2, A11, Th4;
x -' (z -' z) = x by Lm3, Lm4
.= z -' (z -' x) by A1, A14, Lm6 ;
hence (y -' z) - x = [{},(z -' (y -' x))] by A12, A14, Def2
.= (y -' x) - z by A13, Def2 ;
:: thesis: verum
end;
suppose that A15: not x + z <=' y and
A16: ( not y <=' x & not y <=' z ) ; :: thesis: (y -' z) - x = (y -' x) - z
A17: not z <=' y -' x by A1, A15, Lm8;
( not x <=' y -' z & x -' (y -' z) = z -' (y -' x) ) by A15, A16, Lm8, Lm13;
hence (y -' z) - x = [{},(z -' (y -' x))] by Def2
.= (y -' x) - z by A17, Def2 ;
:: thesis: verum
end;
end;