let m be positive Nat; :: thesis: ex a, b, c being positive Nat st card { [x,y] where x, y is positive Nat : (a * x) + (b * y) = c } = m
take 1 ; :: thesis: ex b, c being positive Nat st card { [x,y] where x, y is positive Nat : (1 * x) + (b * y) = c } = m
take 1 ; :: thesis: ex c being positive Nat st card { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = c } = m
take m + 1 ; :: thesis: card { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } = m
set A = { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } ;
set B = { [x,y] where x, y is positive Nat : x + y = m + 1 } ;
{ [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } = { [x,y] where x, y is positive Nat : x + y = m + 1 }

proof

thus { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } c= { [x,y] where x, y is positive Nat : x + y = m + 1 } :: according to XBOOLE_0:def 10 :: thesis: { [x,y] where x, y is positive Nat : x + y = m + 1 } c= { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } or a in { [x,y] where x, y is positive Nat : x + y = m + 1 } )
assume a in { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } ; :: thesis: a in { [x,y] where x, y is positive Nat : x + y = m + 1 }
then ex x, y being positive Nat st
( a = [x,y] & (1 * x) + (1 * y) = m + 1 ) ;
hence a in { [x,y] where x, y is positive Nat : x + y = m + 1 } ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Nat : x + y = m + 1 } or a in { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } )
assume a in { [x,y] where x, y is positive Nat : x + y = m + 1 } ; :: thesis: a in { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 }
then consider x, y being positive Nat such that
A1: ( a = [x,y] & x + y = m + 1 ) ;
(1 * x) + (1 * y) = x + y ;
hence a in { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } by A1; :: thesis: verum

end;

hence card { [x,y] where x, y is positive Nat : (1 * x) + (1 * y) = m + 1 } = m by Th44; :: thesis: verum