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