hereby :: thesis: ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} )
assume y <=' x ; :: thesis: ex IT being Element of REAL+ st IT + y = x
then ex IT being Element of REAL+ st y + IT = x by ARYTM_2:9;
hence ex IT being Element of REAL+ st IT + y = x ; :: thesis: verum
end;
thus ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) by ARYTM_2:20; :: thesis: verum