let x, y be Element of REAL+ ; :: thesis: ( x <=' y implies y -' (y -' x) = x )
assume A1: x <=' y ; :: thesis: y -' (y -' x) = x
y -' x <=' y by Th11;
then (y -' (y -' x)) + (y -' x) = y by Def1
.= (y -' x) + x by A1, Def1 ;
hence y -' (y -' x) = x by ARYTM_2:11; :: thesis: verum