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 :: thesis: ( n1 <= 1 & n2 <= 1 & not ( n1 = 1 & n2 = 0 ) implies ( n1 = 0 & n2 = 1 ) )
A2: ( n1 = 0 implies not n2 = 0 ) by A1;
assume A3: ( n1 <= 1 & n2 <= 1 ) ; :: thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
( n1 = 1 implies not n2 = 1 ) by A1;
hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A3, A2, NAT_1:25; :: 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