let n1, n2 be Nat; :: thesis: ( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )
thus ( not n1 + n2 = 1 or ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) :: thesis: ( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 )

proof

assume A1: n1 + n2 = 1 ; :: thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )

now

assume A2: ( n1 <= 1 & n2 <= 1 ) ; :: thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
A3: ( n1 = 1 implies not n2 = 1 ) by A1;
( n1 = 0 implies not n2 = 0 ) by A1;
hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A2, A3, NAT_1:26; :: thesis: verum

end;

hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A1, Th1; :: thesis: verum

end;

thus ( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 ) ; :: thesis: verum