let a, n be positive Nat; :: thesis: ( 2 <= n implies { [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } is finite )
assume A1: 2 <= n ; :: thesis: { [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } is finite
set A = { [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } ;
defpred S₁[ object , object ] means verum;
set M = (n - 1) -Root a;
set M1 = [/((n - 1) -Root a)\];
n - 1 >= 2 - 1 by A1, XREAL_1:6;
then (n - 1) -Root a >= 0 by PREPOWER:def 2;
then reconsider M1 = [/((n - 1) -Root a)\] as Nat by TARSKI:1;
set B = { [x,y] where x, y is Nat : ( x < M1 & y < M1 & S₁[x,y] ) } ;
A2: { [x,y] where x, y is Nat : ( x < M1 & y < M1 & S₁[x,y] ) } is finite from NUMBER15:sch 1();
{ [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } c= { [x,y] where x, y is Nat : ( x < M1 & y < M1 & S₁[x,y] ) }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } or z in { [x,y] where x, y is Nat : ( x < M1 & y < M1 & S₁[x,y] ) } )
assume z in { [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } ; :: thesis: z in { [x,y] where x, y is Nat : ( x < M1 & y < M1 & S₁[x,y] ) }
then consider x, y being positive Nat such that
A3: z = [x,y] and
A4: (x |^ n) - (y |^ n) = a ;
A5: ( x < (n - 1) -Root a & y < (n - 1) -Root a ) by A1, A4, Th87;
(n - 1) -Root a <= M1 by INT_1:def 7;
then ( x < M1 & y < M1 ) by A5, XXREAL_0:2;
hence z in { [x,y] where x, y is Nat : ( x < M1 & y < M1 & S₁[x,y] ) } by A3; :: thesis: verum

end;

hence { [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } is finite by A2; :: thesis: verum