theorem Th6: :: JORDAN1E:6

for i, j, m, n being Nat st i + j = m + n & i <= m & j <= n holds
i = m