let x, y be Nat; :: thesis: ( not x + y = 1 or ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )
assume A1: x + y = 1 ; :: thesis: ( ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )
x <= 1

proof

assume not x <= 1 ; :: thesis: contradiction
then 1 + 0 < x + y by XREAL_1:8;
hence contradiction by A1; :: thesis: verum

end;

then ( x = 0 or x = 1 ) by NAT_1:25;
hence ( ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) ) by A1; :: thesis: verum