let x, y be Nat; ( not x + y = 1 or ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )
assume A1:
x + y = 1
; ( ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )
x <= 1
proof
assume
not
x <= 1
;
contradiction
then
1
+ 0 < x + y
by XREAL_1:8;
hence
contradiction
by A1;
verum
end;
then
( x = 0 or x = 1 )
by NAT_1:25;
hence
( ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )
by A1; verum