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