let x, y be Element of REAL+ ; :: thesis: ( x <=' y & y <=' x implies x = y )
assume x <=' y ; :: thesis: ( not y <=' x or x = y )
then consider z1 being Element of REAL+ such that
A1: x + z1 = y by ARYTM_2:9;
assume y <=' x ; :: thesis: x = y
then consider z2 being Element of REAL+ such that
A2: y + z2 = x by ARYTM_2:9;
x = x + (z1 + z2) by A1, A2, ARYTM_2:6;
then z1 = {} by Th1, ARYTM_2:5;
hence x = y by A1, ARYTM_2:def 8; :: thesis: verum