let a be Integer; :: thesis: ( 0 divides a iff a = 0 )
( 0 divides a implies a = 0 )

proof

assume 0 divides a ; :: thesis: a = 0
then consider a1 being Integer such that
A1: a = 0 * a1 by INT_1:def 9;
thus a = 0 by A1; :: thesis: verum

end;

hence ( 0 divides a iff a = 0 ) ; :: thesis: verum