theorem :: NUMBER15:84

for x, y, z, t being positive Nat st x <= y & x <= z & z <= t holds
( ( x + y = z * t & z + t = x * y ) iff ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) )