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 lcm b = (x lcm y) ^2 by A1, A2, LmLCM;
hence a lcm b is square ; :: thesis: verum