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