let x, y be Real; :: thesis: ( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
A1: ( x >= 0 iff x + y >= 0 + y ) by XREAL_1:6;
hence ( x >= 0 iff x + y >= y ) ; :: thesis: ( ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
A2: ( x > 0 iff x + y > 0 + y ) by XREAL_1:6;
hence ( x > 0 iff x + y > y ) ; :: thesis: ( ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
thus ( x >= 0 iff y >= y - x ) by A1, XREAL_1:20; :: thesis: ( x > 0 iff y > y - x )
thus ( x > 0 iff y > y - x ) by A2, XREAL_1:19; :: thesis: verum