1 = a gcd 2 by Def3;
hence |.a.| is odd by INT_6:14; :: thesis: verum