let s, t be Element of RAT+ ; :: thesis: s <=' s + t
take t ; :: according to ARYTM_3:def 13 :: thesis: s + t = s + t
thus s + t = s + t ; :: thesis: verum