dom Cart4Id = NATPLUS by FUNCT_2:def 1;
hence { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } is infinite by Th102, CARD_1:59; :: thesis: verum