let a be Integer; :: thesis: ( a is even implies (multiples 2) /\ {a,(a + 1)} = {a} )
set M = multiples 2;
assume A1: a is even ; :: thesis: (multiples 2) /\ {a,(a + 1)} = {a}
thus (multiples 2) /\ {a,(a + 1)} c= {a} :: according to XBOOLE_0:def 10 :: thesis: {a} 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} )
assume A2: x in (multiples 2) /\ {a,(a + 1)} ; :: thesis: x in {a}

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

suppose x = a ; :: thesis: x in {a}

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

end;

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

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

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} or x in (multiples 2) /\ {a,(a + 1)} )
assume x in {a} ; :: thesis: x in (multiples 2) /\ {a,(a + 1)}
then A4: x = a by TARSKI:def 1;
A5: a in multiples 2 by A1, Th76;
a 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