dom exampleSierpinski149 = NATPLUS by PARTFUN1:def 2;
hence { [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 } is infinite by Th96, CARD_1:59; :: thesis: verum