let a be Integer; :: thesis: ( a is odd implies not a is Multiple of 2 )
assume a is odd ; :: thesis: a is not Multiple of 2
hence not 2 divides a ; :: according to NUMBER14:def 15 :: thesis: verum