let r, s be Element of RAT+ ; :: thesis: ex t being Element of RAT+ st
( r + t = s or s + t = r )
( r <=' s or s <=' r ) ;
hence ex t being Element of RAT+ st
( r + t = s or s + t = r ) by Def13; :: thesis: verum