let x, y, z be Element of REAL+ ; ( y <=' x & not y <=' z implies x - (y -' z) = (x -' y) + z )
assume that
A1:
y <=' x
and
A2:
not y <=' z
; x - (y -' z) = (x -' y) + z
y -' z <=' y
by Th11;
then
y -' z <=' x
by A1, Th3;
then
x - (y -' z) = x -' (y -' z)
by Def2;
hence
x - (y -' z) = (x -' y) + z
by A1, A2, Lm12; verum