let a be Integer; :: thesis: card ((multiples 2) /\ {a,(a + 1)}) = 1
( (multiples 2) /\ {a,(a + 1)} = {a} or (multiples 2) /\ {a,(a + 1)} = {(a + 1)} ) by Th79, Th80;
hence card ((multiples 2) /\ {a,(a + 1)}) = 1 by CARD_1:30; :: thesis: verum