let x, y, z be Element of REAL+ ; :: thesis: ( z <=' y implies x + (y -' z) = (x + y) - z )
assume A1: z <=' y ; :: thesis: x + (y -' z) = (x + y) - z
y <=' x + y by ARYTM_2:19;
then z <=' x + y by A1, Th3;
then (x + y) - z = (x + y) -' z by Def2;
hence x + (y -' z) = (x + y) - z by A1, Th13; :: thesis: verum