let m, n be positive Nat; :: thesis: ex a, b, c being Integer st { [x,y] where x, y is Nat : (a * x) + (b * y) = c } = {[m,n]}
consider a being Prime such that
A1: a > m + n by NEWTON:72;
consider b being Prime such that
A2: b > a by NEWTON:72;
take a ; :: thesis: ex b, c being Integer st { [x,y] where x, y is Nat : (a * x) + (b * y) = c } = {[m,n]}
take b ; :: thesis: ex c being Integer st { [x,y] where x, y is Nat : (a * x) + (b * y) = c } = {[m,n]}
take c = (a * m) + (b * n); :: thesis: { [x,y] where x, y is Nat : (a * x) + (b * y) = c } = {[m,n]}
set A = { [x,y] where x, y is Nat : (a * x) + (b * y) = c } ;
set B = {[m,n]};
A3: b > m + n by A1, A2, XXREAL_0:2;
thus { [x,y] where x, y is Nat : (a * x) + (b * y) = c } c= {[m,n]} :: according to XBOOLE_0:def 10 :: thesis: {[m,n]} c= { [x,y] where x, y is Nat : (a * x) + (b * y) = c }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { [x,y] where x, y is Nat : (a * x) + (b * y) = c } or z in {[m,n]} )
assume z in { [x,y] where x, y is Nat : (a * x) + (b * y) = c } ; :: thesis: z in {[m,n]}
then consider x, y being Nat such that
A4: z = [x,y] and
A5: (a * x) + (b * y) = c ;

per cases ( ( m = x & n = y ) or ( x > m & y >= n ) or ( x >= m & y > n ) or x < m or y < n ) by XXREAL_0:1;

suppose ( m = x & n = y ) ; :: thesis: z in {[m,n]}

hence z in {[m,n]} by A4, TARSKI:def 1; :: thesis: verum

end;

suppose ( ( x > m & y >= n ) or ( x >= m & y > n ) ) ; :: thesis: z in {[m,n]}

then ( ( a * x > a * m & b * y >= b * n ) or ( a * x >= a * m & b * y > b * n ) ) by XREAL_1:64, XREAL_1:68;
hence z in {[m,n]} by A5, XREAL_1:8; :: thesis: verum

end;

suppose x < m ; :: thesis: z in {[m,n]}

then A6: m - x > x - x by XREAL_1:8;
then A7: m - x in NAT by INT_1:3;
( b divides b * n & b divides b * y ) ;
then b divides ((a * (m - x)) + (b * n)) - (b * n) by A5, INT_5:1;
then ( b divides a or b divides m - x ) by INT_5:7;
then b <= m - x by A2, A6, A7, NAT_D:7;
then m + n < m - x by A3, XXREAL_0:2;
hence z in {[m,n]} by XREAL_1:6; :: thesis: verum

end;

suppose y < n ; :: thesis: z in {[m,n]}

then A8: n - y > y - y by XREAL_1:8;
then A9: n - y in NAT by INT_1:3;
A10: a > 1 by INT_2:def 4;
( a divides a * m & a divides a * x ) ;
then a divides ((b * (n - y)) + (a * m)) - (a * m) by A5, INT_5:1;
then ( a divides b or a divides n - y ) by INT_5:7;
then a <= n - y by A2, A8, A9, A10, NAT_D:7, INT_2:def 4;
then m + n < n - y by A1, XXREAL_0:2;
hence z in {[m,n]} by XREAL_1:6; :: thesis: verum

end;

end;

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {[m,n]} or z in { [x,y] where x, y is Nat : (a * x) + (b * y) = c } )
assume z in {[m,n]} ; :: thesis: z in { [x,y] where x, y is Nat : (a * x) + (b * y) = c }
then z = [m,n] by TARSKI:def 1;
hence z in { [x,y] where x, y is Nat : (a * x) + (b * y) = c } ; :: thesis: verum