a lcm (a lcm b) = |.a.| lcm |.(a lcm b).| by INT_2:33
.= |.a.| lcm (|.a.| lcm |.b.|) by INT_2:33
.= (|.a.| lcm |.a.|) lcm |.b.| by NEWTON:43
.= a lcm b by INT_2:33 ;
hence a lcm (a lcm b) = a lcm b ; :: thesis: verum