let a be Integer; :: thesis: ( a is odd implies (multiples 2) /\ {a,(a + 1)} = {(a + 1)} )
set M = multiples 2;
assume A1: a is odd ; :: thesis: (multiples 2) /\ {a,(a + 1)} = {(a + 1)}
thus (multiples 2) /\ {a,(a + 1)} c= {(a + 1)} :: according to XBOOLE_0:def 10 :: thesis: {(a + 1)} c= (multiples 2) /\ {a,(a + 1)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (multiples 2) /\ {a,(a + 1)} or x in {(a + 1)} )
assume A2: x in (multiples 2) /\ {a,(a + 1)} ; :: thesis: x in {(a + 1)}

per cases then ( x = a + 1 or x = a ) by TARSKI:def 2;

suppose x = a + 1 ; :: thesis: x in {(a + 1)}

hence x in {(a + 1)} by TARSKI:def 1; :: thesis: verum

end;

suppose A3: x = a ; :: thesis: x in {(a + 1)}

reconsider x = x as Multiple of 2 by A2, Th61;
2 divides x by Def15;
hence x in {(a + 1)} by A3, A1; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(a + 1)} or x in (multiples 2) /\ {a,(a + 1)} )
assume x in {(a + 1)} ; :: thesis: x in (multiples 2) /\ {a,(a + 1)}
then A4: x = a + 1 by TARSKI:def 1;
A5: a + 1 in multiples 2 by A1, Th76;
a + 1 in {a,(a + 1)} by TARSKI:def 2;
hence x in (multiples 2) /\ {a,(a + 1)} by A4, A5, XBOOLE_0:def 4; :: thesis: verum