consider x being Nat such that
A1: a = x ^2 by PYTHTRIP:def 3;
consider y being Nat such that
A2: b = y ^2 by PYTHTRIP:def 3;
a gcd b = (x gcd y) ^2 by A1, A2, NEWTON02:7;
hence a gcd b is square ; :: thesis: verum