theorem :: NUMBER14:81
for a being Integer holds
( (multiples 2) /\ {a,(a + 1)} = {a} or (multiples 2) /\ {a,(a + 1)} = {(a + 1)} ) by Th79, Th80;