let x, y be Element of REAL+ ; :: thesis: ex z being Element of REAL+ st
( x + z = y or y + z = x )
( x <=' y or y <=' x ) ;
hence ex z being Element of REAL+ st
( x + z = y or y + z = x ) by Th9; :: thesis: verum