let n, n1, n2 be Nat; :: thesis: ( ( n1 > n or n2 > n ) implies n1 + n2 > n )
A1: ( n1 > n & n2 >= 0 implies n1 + n2 > n + 0 ) by XREAL_1:8;
A2: ( n1 >= 0 & n2 > n implies n1 + n2 > n + 0 ) by XREAL_1:8;
assume ( n1 > n or n2 > n ) ; :: thesis: n1 + n2 > n
hence n1 + n2 > n by A1, A2; :: thesis: verum