theorem Th79: :: NUMBER14:79
for a being Integer st a is even holds
(multiples 2) /\ {a,(a + 1)} = {a}