let x, y be Element of REAL+ ; :: thesis: ( x <=' y & y = {} implies x = {} )
assume x <=' y ; :: thesis: ( not y = {} or x = {} )
then ex z being Element of REAL+ st x + z = y by ARYTM_2:9;
hence ( not y = {} or x = {} ) by ARYTM_2:5; :: thesis: verum