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