let x, y be Element of REAL+ ; :: thesis: ( x = {} implies x <=' y )
assume x = {} ; :: thesis: x <=' y
then x + y = y by ARYTM_2:def 8;
hence x <=' y by ARYTM_2:19; :: thesis: verum