let n be non zero Nat; :: thesis: for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x lcm y in NatDivisors n
let x, y be Nat; :: thesis: ( x in NatDivisors n & y in NatDivisors n implies x lcm y in NatDivisors n )
assume a0: ( x in NatDivisors n & y in NatDivisors n ) ; :: thesis: x lcm y in NatDivisors n
then ( x divides n & y divides n & x > 0 & y > 0 ) by MOEBIUS1:39;
then x lcm y divides n by NAT_D:def 4;
hence x lcm y in NatDivisors n by a0, MOEBIUS1:39; :: thesis: verum