let k be Nat; :: thesis: for i, n, m, r being Integer st k <> i holds
divisors (n,m,k) misses divisors (n,m,i)
let i be Integer; :: thesis: for n, m, r being Integer st k <> i holds
divisors (n,m,k) misses divisors (n,m,i)
let n, m, r be Integer; :: thesis: ( k <> i implies divisors (n,m,k) misses divisors (n,m,i) )
assume A1: k <> i ; :: thesis: divisors (n,m,k) misses divisors (n,m,i)
assume divisors (n,m,k) meets divisors (n,m,i) ; :: thesis: contradiction
then consider x being object such that
A2: ( x in divisors (n,m,k) & x in divisors (n,m,i) ) by XBOOLE_0:3;
reconsider x = x as Nat by A2;
( x mod m = k & x mod m = i ) by A2, Th12;
hence contradiction by A1; :: thesis: verum