let r, s be Element of RAT+ ; :: thesis: ( r <=' s & s <=' r implies r = s )
given x being Element of RAT+ such that A1: s = r + x ; :: according to ARYTM_3:def 13 :: thesis: ( not s <=' r or r = s )
given y being Element of RAT+ such that A2: r = s + y ; :: according to ARYTM_3:def 13 :: thesis: r = s
r + {} = r by Th50
.= r + (x + y) by A1, A2, Th51 ;
then x = {} by Th62, Th63;
hence r = s by A1, Th50; :: thesis: verum