let a, b be Integer; :: thesis: ( ( a = 0 & b = 0 ) iff a gcd b = 0 )
0 divides 0 gcd 0 by Def2;
hence ( a = 0 & b = 0 implies a gcd b = 0 ) ; :: thesis: ( a gcd b = 0 implies ( a = 0 & b = 0 ) )
assume a gcd b = 0 ; :: thesis: ( a = 0 & b = 0 )
then ( 0 divides a & 0 divides b ) by Def2;
hence ( a = 0 & b = 0 ) ; :: thesis: verum