reconsider t = sqrt a, q = sqrt b as Element of NAT by ORDINAL1:def 12;
A1: ( t ^2 = a & q ^2 = b ) by SQUARE_1:def 2;
(t ^2) lcm (q ^2) = (t lcm q) ^2 by LmLCM;
hence a lcm b is square by A1; :: thesis: verum