let a be Integer; :: thesis: ( a is odd implies not a in multiples 2 )
assume A1: a is odd ; :: thesis: not a in multiples 2
assume a in multiples 2 ; :: thesis: contradiction
then a is Multiple of 2 by Th61;
hence contradiction by A1, Th77; :: thesis: verum