let a, x, k be Nat; :: thesis: ( k > 0 & x divides a + k & x divides a - k implies x <= 2 * k )
assume A1: k > 0 ; :: thesis: ( not x divides a + k or not x divides a - k or x <= 2 * k )
( x divides a + k & x divides a - k implies ( x divides 2 * a & x divides 2 * k ) ) by Th22;
hence ( not x divides a + k or not x divides a - k or x <= 2 * k ) by A1, NAT_D:7; :: thesis: verum