theorem Th3: :: FLANG_1:3

for n1, n2 being Nat holds
( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )