let i, j be Nat; :: thesis: ( i,j are_coprime implies i lcm j = i * j )
reconsider ii = i, jj = j as Integer ;
|.(ii * jj).| = ii * jj by ABSVALUE:def 1;
hence ( i,j are_coprime implies i lcm j = i * j ) by INT_6:15; :: thesis: verum