for i1, i2, i3, i4, c being Nat st i1 <= c & i2 <= c & i3 <= c & i4 <= c & not ((i1 + i2) + i3) + i4 < 4 * c holds
( i1 = c & i2 = c & i3 = c & i4 = c )