let a be Integer; :: thesis: ( a is even implies a in multiples 2 )
assume a is even ; :: thesis: a in multiples 2
then a is Multiple of 2 by Th75;
hence a in multiples 2 ; :: thesis: verum