hereby :: thesis: ( not y <=' x implies ex b₁ being Element of REAL+ st b₁ = {} )

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 b₁ being Element of REAL+ st b₁ = {} ) by ARYTM_2:20; :: thesis: verum