dom exampleSierpinski196 = NAT by PARTFUN1:def 2;
hence { [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) } is infinite by Th85, CARD_1:59; :: thesis: verum