let x, y be Element of REAL+ ; :: thesis: ( x = {} implies y -' x = y )
assume A1: x = {} ; :: thesis: y -' x = y
then A2: x <=' y by Th6;
thus y -' x = (y -' x) + x by A1, ARYTM_2:def 8
.= y by A2, Def1 ; :: thesis: verum