let a, c be Nat; :: thesis: for b being non zero Nat st a * b < c & c < a * (b + 1) holds
( not a divides c & not c divides a )
let b be non zero Nat; :: thesis: ( a * b < c & c < a * (b + 1) implies ( not a divides c & not c divides a ) )
assume A1: ( a * b < c & c < a * (b + 1) ) ; :: thesis: ( not a divides c & not c divides a )
then reconsider c = c as non zero Nat ;
reconsider a = a as non zero Nat by A1;
assume ( a divides c or c divides a ) ; :: thesis: contradiction

per cases then ( a divides c or c divides a ) ;

suppose a divides c ; :: thesis: contradiction

then consider k being Nat such that
B1: c = a * k by NAT_D:def 3;
b < k by A1, B1, XREAL_1:64;
then b + 1 <= k by NAT_1:13;
hence contradiction by A1, B1, XREAL_1:64; :: thesis: verum

end;

suppose B1: c divides a ; :: thesis: contradiction

a * b >= a * 1 by XREAL_1:64, NAT_1:14;
then c > a by A1, XXREAL_0:2;
hence contradiction by B1, NAT_D:7; :: thesis: verum

end;

end;