theorem :: ACKERMAN:47

for m, n1, n2 being Nat st 1 <= n1 & n1 <= m & 1 <= n2 & n2 <= m & m proj n1 = m proj n2 holds
n1 = n2