theorem Th80: :: NUMBER14:80

for a being Integer st a is odd holds
(multiples 2) /\ {a,(a + 1)} = {(a + 1)}