let x, y, z be Element of REAL+ ; :: thesis: (y -' z) -' x = (y -' x) -' z
thus (y -' z) -' x = y -' (x + z) by Lm9
.= (y -' x) -' z by Lm9 ; :: thesis: verum