let m be positive Nat; :: thesis: card { [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } = m
set A = { [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } ;
set B = { [x,y] where x, y is positive Nat : x + y = m + 1 } ;
{ [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } = { [x,y] where x, y is positive Nat : x + y = m + 1 }

proof

thus { [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } 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 : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } 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 : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } ; :: thesis: a in { [x,y] where x, y is positive Nat : x + y = m + 1 }
then consider x, y being positive Nat such that
A1: a = [x,y] and
A2: ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 ;
((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = (((x + y) - m) - 1) * ((x + y) + 1) ;
then ((x + y) - m) - 1 = 0 by A2;
hence a in { [x,y] where x, y is positive Nat : x + y = m + 1 } by A1; :: 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 : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } )
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 : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 }
then consider x, y being positive Nat such that
A3: ( a = [x,y] & x + y = m + 1 ) ;
((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = (((x + y) - m) - 1) * ((x + y) + 1) ;
hence a in { [x,y] where x, y is positive Nat : ((((((x ^2) + (y ^2)) + ((2 * x) * y)) - (m * x)) - (m * y)) - m) - 1 = 0 } by A3; :: thesis: verum

end;

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