for x, y being Nat holds
( y = x ! iff ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) )