let x, y be Element of REAL+ ; :: thesis: ( x <=' y & y = {} implies x = {} )
assume x <=' y ; :: thesis: ( not y = {} or x = {} )
then consider z being Element of REAL+ such that
A1: x + z = y by ARYTM_2:10;
thus ( not y = {} or x = {} ) by A1, ARYTM_2:6; :: thesis: verum