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