let a, b be Integer; :: thesis: ( a < b implies { n where n is Nat : a + n,b + n are_coprime } is infinite )
assume A1: a < b ; :: thesis: { n where n is Nat : a + n,b + n are_coprime } is infinite
set S = { n where n is Nat : a + n,b + n are_coprime } ;
defpred S₁[ Nat, object ] means ex k being Nat st
( 0 < (((b - a) * k) + 1) - a & $1 <= (((b - a) * k) + 1) - a & $2 = (((b - a) * k) + 1) - a );
A2: for i being Element of NAT ex j being object st S₁[i,j]

proof

let i be Element of NAT ; :: thesis: ex j being object st S₁[i,j]
consider k being Nat such that
A3: i < (((b - a) * k) + 1) - a and
k = |.[/((((i + a) - 1) / (b - a)) + 1)\].| by A1, Th17;
take (((b - a) * k) + 1) - a ; :: thesis: S₁[i,(((b - a) * k) + 1) - a]
take k ; :: thesis: ( 0 < (((b - a) * k) + 1) - a & i <= (((b - a) * k) + 1) - a & (((b - a) * k) + 1) - a = (((b - a) * k) + 1) - a )
thus ( 0 < (((b - a) * k) + 1) - a & i <= (((b - a) * k) + 1) - a & (((b - a) * k) + 1) - a = (((b - a) * k) + 1) - a ) by A3; :: thesis: verum

end;

consider f being ManySortedSet of NAT such that
A4: for i being Element of NAT holds S₁[i,f . i] from PBOOLE:sch 6(A2);
set R = rng f;
A5: dom f = NAT by PARTFUN1:def 2;
A6: rng f c= { n where n is Nat : a + n,b + n are_coprime }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in { n where n is Nat : a + n,b + n are_coprime } )
assume x in rng f ; :: thesis: x in { n where n is Nat : a + n,b + n are_coprime }
then consider t being object such that
A7: t in dom f and
A8: x = f . t by FUNCT_1:def 3;
reconsider t = t as Element of NAT by A7, PARTFUN1:def 2;
S₁[t,f . t] by A4;
then consider k being Nat such that
A9: 0 < (((b - a) * k) + 1) - a and
A10: f . t = (((b - a) * k) + 1) - a ;
reconsider n = (((b - a) * k) + 1) - a as Nat by A9;
A11: 0 < b - a by A1, XREAL_1:50;
then reconsider an = a + n as Element of NAT by INT_1:3;
0 <= ((b - a) * (k + 1)) + 1 by A11;
then reconsider bn = b + n as Element of NAT by INT_1:3;
A12: ( 1 divides an & 1 divides bn ) by INT_2:12;
for d being Integer st d divides an & d divides bn holds
d divides 1

proof

let d be Integer; :: thesis: ( d divides an & d divides bn implies d divides 1 )
assume that
A13: d divides an and
A14: d divides bn ; :: thesis: d divides 1
A15: an - ((b - a) * k) = 1 ;
A16: a - b = - (b - a) ;
d divides an - bn by A13, A14, INT_5:1;
then d divides b - a by A16, INT_2:10;
then d divides (b - a) * k by INT_2:2;
hence d divides 1 by A13, A15, INT_5:1; :: thesis: verum

end;

then a + n,b + n are_coprime by A12, INT_2:def 2;
hence x in { n where n is Nat : a + n,b + n are_coprime } by A8, A10; :: thesis: verum

end;

for m being Nat ex N being Nat st
( N >= m & N in rng f )

proof

let m be Nat; :: thesis: ex N being Nat st
( N >= m & N in rng f )
consider k being Nat such that
A17: 0 < (((b - a) * k) + 1) - a and
A18: m + 1 <= (((b - a) * k) + 1) - a and
A19: f . (m + 1) = (((b - a) * k) + 1) - a by A4;
reconsider N = (((b - a) * k) + 1) - a as Element of NAT by A17, ORDINAL1:def 12;
take N ; :: thesis: ( N >= m & N in rng f )
m + 0 <= m + 1 by XREAL_1:6;
hence N >= m by A18, XXREAL_0:2; :: thesis: N in rng f
thus N in rng f by A5, A19, FUNCT_1:def 3; :: thesis: verum

end;

hence { n where n is Nat : a + n,b + n are_coprime } is infinite by A6, PYTHTRIP:9; :: thesis: verum