let k be Nat; :: thesis: for n, m, r, p being Integer holds
( k in (divisors (n,m,r)) \/ (divisors (n,m,p)) iff ( ( k mod m = r or k mod m = p ) & k divides n ) )
let n, m, r, p be Integer; :: thesis: ( k in (divisors (n,m,r)) \/ (divisors (n,m,p)) iff ( ( k mod m = r or k mod m = p ) & k divides n ) )

hereby :: thesis: ( ( k mod m = r or k mod m = p ) & k divides n implies k in (divisors (n,m,r)) \/ (divisors (n,m,p)) )

assume k in (divisors (n,m,r)) \/ (divisors (n,m,p)) ; :: thesis: ( ( k mod m = r or k mod m = p ) & k divides n )
then ( k in divisors (n,m,r) or k in divisors (n,m,p) ) by XBOOLE_0:def 3;
hence ( ( k mod m = r or k mod m = p ) & k divides n ) by Th12; :: thesis: verum

end;

assume ( ( k mod m = r or k mod m = p ) & k divides n ) ; :: thesis: k in (divisors (n,m,r)) \/ (divisors (n,m,p))
then ( k in divisors (n,m,r) or k in divisors (n,m,p) ) ;
hence k in (divisors (n,m,r)) \/ (divisors (n,m,p)) by XBOOLE_0:def 3; :: thesis: verum