let x, y be Real; ( ( 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 )
; ( ( 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 )
; ( ( 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; ( x > 0 iff y > y - x )
thus
( x > 0 iff y > y - x )
by A2, XREAL_1:19; verum