let i, j be natural Number ; :: thesis: ( i + j = 0 implies ( i = 0 & j = 0 ) )
( 0 <= i & 0 <= j ) by Th2;
hence ( i + j = 0 implies ( i = 0 & j = 0 ) ) ; :: thesis: verum