theorem Th1: :: GAUSSINT:1

for x, y being Nat holds
( not x + y = 1 or ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )