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 A2: z <=' x + y by A1, Th3;
(x + (y -' z)) + z = x + ((y -' z) + z) by ARYTM_2:6
.= x + y by A1, Def1
.= ((x + y) -' z) + z by A2, Def1 ;
hence x + (y -' z) = (x + y) -' z by ARYTM_2:11; :: thesis: verum