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